lift_mk_one — Mathlib

English

The identity map of a localized module is localized; i.e., LinearMap.id on M localizes.

Русский

Идентичность локализованного модуля локализуется; то есть LinearMap.id локализуется.

LaTeX

$$$[IsLocalizedModule S \\; \\mathrm{id}].$$$

Lean4

@[simp]
theorem lift_mk_one (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (m : M) :
    (LocalizedModule.lift S g h) (LocalizedModule.mk m 1) = g m := by simp [lift_mk]

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