mk'_eq_mk' — Mathlib

English

Equality of mk' with the linear-map version: IsLocalization.mk' A x s equals IsLocalizedModule.mk' (Algebra.linearMap R A) x s.

Русский

Равенство mk' в локализации и в виде линейного отображения: IsLocalization.mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s.

LaTeX

$$$\\IsLocalization.mk' A x s = \\IsLocalizedModule.mk' (Algebra.linearMap R A) x s.$$$

Lean4

/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`. -/
theorem mk'_eq_mk' [IsLocalization S A] (x : R) (s : S) :
    IsLocalization.mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s :=
  by
  rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']
  exact IsLocalization.smul_mk'_self

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