English
The composition of the toProd map with the corresponding (inverse) ofProd map is the identity on the Clifford algebra of the product; i.e., toProd ∘ ofProd = id.
Русский
Композицией отображения toProd с соответствующим обратно действующим ofProd является тождество на Clifford-алгебре произведения: toProd ∘ ofProd = id.
LaTeX
$$$$ (toProd Q_1 Q_2) \\circ (\\text{ofProd } Q_1 Q_2) = \\mathrm{AlgHom.id} (CliffordAlgebra (QuadraticMap.prod Q_1 Q_2)) $$$$
Lean4
theorem toProd_comp_ofProd : (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id _ _ :=
by
ext m <;> dsimp
· rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero, LinearMap.map_zero, add_zero]
· rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero, LinearMap.map_zero, zero_add]
