English
Let h and h' be proofs that certain BilinearForms correspond to quadratic maps differing by Q' − Q and Q'' − Q' respectively. Then for all x in CliffordAlgebra Q, applying changeForm h followed by changeForm h' is the same as changeForm of the sum proof, i.e., changeForm h' (changeForm h x) = changeForm (changeForm.add_proof h h') x.
Русский
Пусть существуют доказательства h и h', что соответствующие билинные формы соответствуют квадратичным картам Q' − Q и Q'' − Q' соответственно. Тогда для любого x в CliffordAlgebra Q выполнено: применение changeForm h, затем changeForm h' эквивалентно changeForm от суммы доказательств.
LaTeX
$$$ \\text{changeForm}_{h'}(\\text{changeForm}_{h}(x)) = \\text{changeForm}_{\\text{changeForm.add\_proof}(h,h')}(x) $$$
Lean4
/-- This is [bourbaki2007][] $9 Lemma 3. -/
theorem changeForm_changeForm (x : CliffordAlgebra Q) :
changeForm h' (changeForm h x) = changeForm (changeForm.add_proof h h') x := by
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [changeForm_algebraMap]
| add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
| ι_mul _ _ hx =>
rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub, LinearMap.add_apply, map_add,
LinearMap.add_apply, changeForm_contractLeft, hx, add_comm (_ : CliffordAlgebra Q'')]
