English
If h and h′ relate B to Q′−Q and B′ to Q″−Q′, then changeFormEquiv h gives a linear equivalence between CliffordAlgebra Q and CliffordAlgebra Q′; its inverse is changeForm with the proof that B′ is the corresponding form.
Русский
Если h и h′ задают переходы между формами, то changeFormEquiv h образует линейное эквивалент между CliffordAlgebra(Q) и CliffordAlgebra(Q′); обратное — changeForm с доказательством корректности h′.
LaTeX
$$$\\text{changeFormEquiv}(h) : CliffordAlgebra(Q) \\simeq_\\!R CliffordAlgebra(Q')$, invFun = changeForm(\\text{changeForm.neg_proof}(h)).$$
Lean4
/-- Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules.
This is $\bar \lambda_B$ from [bourbaki2007][] $9 Proposition 3. -/
@[simps apply]
def changeFormEquiv : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q' :=
{ changeForm h with
toFun := changeForm h
invFun := changeForm (changeForm.neg_proof h)
left_inv := fun x => by
exact (changeForm_changeForm _ _ x).trans <| by simp_rw [(add_neg_cancel B), changeForm_self_apply]
right_inv := fun x => by
exact (changeForm_changeForm _ _ x).trans <| by simp_rw [(neg_add_cancel B), changeForm_self_apply] }
