mk_eq_mk' — Mathlib

English

The two canonical ways of forming a localization element, mk and IsLocalization.mk' (Localization M), are identical. In particular, mk equals IsLocalization.mk' (Localization M).

Русский

Два канонических способа формирования локализационного элемента mk и IsLocalization.mk' (Localization M) совпадают. То есть mk = IsLocalization.mk' (Localization M).

LaTeX

$$$\\mathrm{mk} = \\mathrm{IsLocalization.mk'}\\ (\\mathrm{Localization}\\ M)$$$

Lean4

theorem mk_eq_mk' : (mk : R → M → Localization M) = IsLocalization.mk' (Localization M) :=
  mk_eq_monoidOf_mk'

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