toProd_ι_tmul_one — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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