mul_algebraMap₀ — Mathlib

English

For all n, r ∈ R and a ∈ ⨂[R]^n M, the scalar action of r on a coincides with multiplying a by algebraMap₀ r in the tensor power.

Русский

Для всех n, r ∈ R и a ∈ ⨂[R]^n M скалярное умножение r на a совпадает с умножением a на algebraMap₀ r в тензорной степени.

LaTeX

$$$ (algebraMap_0\\; r) \\cdot a = r \\cdot a \\quad (a \\in ⨂[R]^n M) $$$

Lean4

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

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