map_smul — Mathlib

English

Let a ∈ S and x ∈ S be elements such that the localization maps respect multiplication by a, i.e., the localization map commutes with the scalar action of elements from R on S.

Русский

Пусть a ∈ S и x ∈ S так, что локализационное отображение сохранено под умножением на a, то есть отражение локализации сохраняет скалярную операцию элементов из R над S.

LaTeX

$$$$\\mathrm{map}_Q(g, hy)(z \\cdot x) = g(z) \\cdot \\mathrm{map}_Q(g, hy)(x)$$$$

Lean4

protected theorem map_smul (x : S) (z : R) : map Q g hy (z • x : S) = g z • map Q g hy x := by
  rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul, map_eq]

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