ofProd_ι_mk — Mathlib

English

In the product Clifford algebra, the image of the embedding ι applied to the pair (m1, m2) equals the sum of the left and right embeddings: ι Q1 m1 ⊗ 1 plus 1 ⊗ ι Q2 m2.

Русский

В произведении Clifford-алгебр образ отображения ι применительно к паре (m1, m2) равен сумме левого и правого внедрения: ι Q1 m1 ⊗ 1 плюс 1 ⊗ ι Q2 m2.

LaTeX

$$$$\\text{ofProd } Q_1 Q_2\\ (\\iota\\_ Q_1 m_1 \\; ᵍ\\otimes_\\mathrm{t} \\; 1) = \\iota\\_ Q_1 m_1 \; ᵍ\\otimes_\\mathrm{t} \\; 1 + 1 \\; ᵍ\\otimes_\\mathrm{t} \\; \\iota\\_ Q_2 m_2$$$$

Lean4

@[simp]
theorem ofProd_ι_mk (m₁ : M₁) (m₂ : M₂) : ofProd Q₁ Q₂ (ι _ (m₁, m₂)) = ι Q₁ m₁ ᵍ⊗ₜ1 + 1 ᵍ⊗ₜι Q₂ m₂ :=
  by
  rw [ofProd, lift_ι_apply]
  rfl

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