algebraMap₀_mul_algebraMap₀ — Mathlib

English

The map algebraMap₀ is multiplicative: algebraMap₀(r s) equals algebraMap₀(r) algebraMap₀(s) inside the tensor power.

Русский

Отображение algebraMap₀ сохраняет умножение: algebraMap₀(rs) равно algebraMap₀(r) algebraMap₀(s) внутри тензорного произведения.

LaTeX

$$$ \\operatorname{algebraMap}_0(r s) = \\operatorname{algebraMap}_0(r) \\operatorname{algebraMap}_0(s) $$$

Lean4

theorem algebraMap₀_mul_algebraMap₀ (r s : R) :
    cast R M (add_zero _) (algebraMap₀ r ₜ* algebraMap₀ s) = algebraMap₀ (r * s) :=
  by
  rw [← smul_eq_mul, LinearEquiv.map_smul]
  exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

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