English
For any x ∈ R and y ∈ M (viewed as a unit in Localization), the element mk x y in Localization M coincides with IsLocalization.mk' (Localization M) x y. In other words, two natural constructions of a localization element agree.
Русский
Для любых x ∈ R и y ∈ M (как элемент Localization), элемент mk x y в Localization M равен IsLocalization.mk' (Localization M) x y. Иными словами, coincide две естественные конструкции локализационного элемента.
LaTeX
$$$\\forall x:\\, R\\ \\forall y:\\, \\{m:\\, M\\mid \\text{membership}\\},\\ \n \\mathrm{mk}\\ x\\ y = \\mathrm{IsLocalization.mk'}\\ (\\mathrm{Localization}\\ M)\\ x\\ y$$$
Lean4
theorem mk_eq_mk'_apply (x y) : mk x y = IsLocalization.mk' (Localization M) x y := by
rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]
