toProd_one_tmul_ι — Mathlib

English

The embedding of m2 from M2 into the product Clifford algebra corresponds to the right component embedding, i.e., toProd Q1 Q2 (1 ⊗ ι Q2 m2) = ι (prod) (0, m2).

Русский

Встраивание в произведение Clifford-алгебры элемента из M2 соответствует правому компоненту: toProd Q1 Q2 (1 ⊗ ι Q2 m2) = ι (prod) (0, m2).

LaTeX

$$$$\\text{toProd } Q_1 Q_2\\ (1 \\ ᵍ\\otimes_\\mathrm{t} \\ ι\\_ Q_2 m_2) = ι\\_ (QuadraticMap.prod Q_1 Q_2)\\ (0, m_2)$$$$

Lean4

@[simp]
theorem toProd_one_tmul_ι (m₂ : M₂) : toProd Q₁ Q₂ (1 ᵍ⊗ₜι _ m₂) = ι _ (0, m₂) := by
  rw [toProd, GradedTensorProduct.lift_tmul, map_one, one_mul, map_apply_ι, QuadraticMap.Isometry.inr_apply]

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