ofProd_comp_toProd — Mathlib

English

The composition of the (ofProd Q1 Q2) with the (toProd Q1 Q2) map is the identity on the graded tensor product CliffordAlgebra; i.e., (ofProd Q1 Q2) ∘ (toProd Q1 Q2) = id.

Русский

Композицией (ofProd Q1 Q2) с (toProd Q1 Q2) является тождество на GradedTensorProduct; (ofProd Q1 Q2) ∘ (toProd Q1 Q2) = id.

LaTeX

$$$$ (\\text{ofProd } Q_1 Q_2) \\circ (\\text{toProd } Q_1 Q_2) = \\mathrm{AlgHom.id} (CliffordAlgebra (QuadraticMap.prod Q_1 Q_2)) $$$$

Lean4

theorem ofProd_comp_toProd : (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id _ _ := by ext <;> simp

Похожие утверждения