ι_eq_v_add_smul_e0 — Mathlib

English

For any m ∈ M and r ∈ R, the image of (m,r) under the canonical embedding ι into the enlarged Clifford algebra decomposes as the sum of the embedded original vector and a scalar multiple of the new dimension vector: ι(Q' Q)(m,r) = v(Q) m + r · e0(Q).

Русский

Для любого m ∈ M и r ∈ R образ (m, r) через каноническое вложение ι в enlarge-Clifford алгебру разлагается как сумма образа исходного вектора и скалярного множителя нового вектора размерности: ι(Q' Q)(m, r) = v(Q) m + r · e0(Q).

LaTeX

$$$\iota(Q' Q)(m,r) = v(Q)\,m + r \cdot e_0(Q)$$$

Lean4

theorem ι_eq_v_add_smul_e0 (m : M) (r : R) : ι (Q' Q) (m, r) = v Q m + r • e0 Q := by
  rw [e0, v, LinearMap.comp_apply, LinearMap.inl_apply, ← LinearMap.map_smul, Prod.smul_mk, smul_zero, smul_eq_mul,
    mul_one, ← LinearMap.map_add, Prod.mk_add_mk, zero_add, add_zero]

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