fromLocalizedModule'_smul — Mathlib

English

The action of R on the localized module commutes with the localization map: r · fromLocalizedModule'(x) = fromLocalizedModule'(r · x).

Русский

Действие элементов из R на локализованный модуль коммутирует с отображением локализации: r · fromLocalizedModule'(x) = fromLocalizedModule'(r · x).

LaTeX

$$$$ r \cdot \mathrm{fromLocalizedModule}'(x) = \mathrm{fromLocalizedModule}'(r \cdot x). $$$$

Lean4

theorem fromLocalizedModule'_smul (r : R) (x : LocalizedModule S M) :
    r • fromLocalizedModule' S f x = fromLocalizedModule' S f (r • x) :=
  LocalizedModule.induction_on
    (by
      intro a b
      rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk, f.map_smul, map_smul])
    x

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