algebraMap₀_mul — Mathlib

English

For any r ∈ R and a ∈ ⨂[R]^n M, the product of algebraMap₀ r with a corresponds to the scalar action r • a via the natural cast to M.

Русский

Пусть r ∈ R и a ∈ ⨂[R]^n M. Произведение algebraMap₀(r) с a совпадает с действием скаляра r • a после соответствующего отображения в M.

LaTeX

$$$ \\text{cast } R\\!\\!M (\\operatorname{zero\_add}) (\\operatorname{algebraMap}_0(r) \\otimes a) = r \\cdot a \\; (a \\in \\; \\⨂[R]^n M)$$$

Lean4

theorem algebraMap₀_mul {n} (r : R) (a : ⨂[R]^n M) : cast R M (zero_add _) (algebraMap₀ r ₜ* a) = r • a := by
  rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, LinearEquiv.map_smul, ←
    gMul_eq_coe_linearMap, one_mul]

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