English
The composition of the even-to-new-dimension maps is the identity on the corresponding subalgebra, expressing that the embedding is an isomorphism on the even part.
Русский
Композиция отображений, переводящих между четной подалгеброй и новой размерностью, равна идентичности; вложение является изоморфизмом на четной части.
LaTeX
$$$(toEven\ Q) \circ (ofEven\ Q) = \mathrm{Id}$ on the appropriate subalgebra$$
Lean4
theorem toEven_ι (m : M) : (toEven Q (ι Q m) : CliffordAlgebra (Q' Q)) = e0 Q * v Q m :=
by
rw [toEven, CliffordAlgebra.lift_ι_apply]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
erw [LinearMap.codRestrict_apply]
rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
