contractLeft_algebraMap_mul — Mathlib

English

The contraction operator is linear over the base ring with respect to left algebra maps: for r ∈ R and b ∈ Clifford(Q), d ⌋ (algebraMap r · b) = algebraMap r · (d ⌋ b).

Русский

Свёртывание линейно относительно базового кольца по луще отображению алгебраMap: для r ∈ R и b ∈ Clifford(Q) имеем $ d ⌋ (algebraMap r · b) = algebraMap r · (d ⌋ b) $.

LaTeX

$$$ d\\lbrack algebraMap R (CliffordAlgebra Q) \\; b = algebraMap R (CliffordAlgebra Q) \\; r \\cdot (d\\lbrack b) $$$

Lean4

theorem contractLeft_algebraMap_mul (r : R) (b : CliffordAlgebra Q) :
    d⌋(algebraMap _ _ r * b) = algebraMap _ _ r * (d⌋b) := by rw [← Algebra.smul_def, map_smul, Algebra.smul_def]

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