∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q Q' : QuadraticForm R M),
  Q' = -Q → ∀ (m : M), ((-(CliffordAlgebra.even.ι Q').bilin) m) m = (algebraMap R ↥(CliffordAlgebra.even Q')) (Q m)