contractRight_algebraMap_mul — Mathlib

English

Contraction on the right commutes with left algebra multiplication by an element r ∈ R: contractRight (algebraMap r) b = algebraMap r · contractRight b.

Русский

Свёртывание справа коммутирует с левым умножением на скаляр: contractRight(algebraMap r) b = algebraMap r · contractRight b.

LaTeX

$$$ contractRight\\_algebraMap\\_mul(R, Q, d, r, b) :\\ d\\lbrack algebraMap R (CliffordAlgebra Q) r \\; \\cdot b = algebraMap R (CliffordAlgebra Q) r \\cdot (d\\lbrack b) $$$

Lean4

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

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