English
The composition of two change of form maps corresponds to the change form for the sum-contracted bilinear data: (changeForm h').compose (changeForm h) = changeForm (changeForm.add_proof h h').
Русский
Составление двух отображений смены формы равно смене формы для суммы конракций: (changeForm h').comp (changeForm h) = changeForm (changeForm.add_proof h h').
LaTeX
$$$ (\text{changeForm}(h')).comp (\text{changeForm}(h)) = \text{changeForm}(\text{changeForm.add_proof}(h,h')) $$$
Lean4
/-- Theorem 23 of [grinberg_clifford_2016][] -/
theorem changeForm_contractLeft (d : Module.Dual R M) (x : CliffordAlgebra Q) :
changeForm h (d⌋x) = d⌋(changeForm h x) := by
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]
| add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy]
| ι_mul _ _ hx =>
simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, LinearMap.map_smul]
rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]
