mk_eq_monoidOf_mk' — Mathlib

English

For any x ∈ M, the canonical mk map into localization Away from x coincides with the canonical mk' map arising from Away.monoidOf x; i.e., mk = (Away.monoidOf x).mk'.

Русский

Пусть x ∈ M. Каноническое отображение mk в локализации Away от x совпадает с каноническим отображением mk', полученным из Away.monoidOf x; то есть mk = (Away.monoidOf x).mk'.

LaTeX

$$$ mk = (Away.monoidOf x).mk' $$$

Lean4

@[to_additive]
theorem mk_eq_monoidOf_mk' : mk = (Away.monoidOf x).mk' := by simp [Localization.mk_eq_monoidOf_mk']

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