English
There is a canonical monoid hom from M × S to Localization(S) sending (m,s) to mk(m,s). This monoid hom preserves identity and multiplication.
Русский
Существуют канонические моноид-гомоморфизм из M × S в Localization(S), отображающий (m,s) в mk(m,s) и сохраняющий единицу и умножение.
LaTeX
$$$\\mathrm{mkHom}: (M \\times S) \\to \\mathrm{Localization}(S),\\quad \\mathrm{mkHom}(1,1)=1,\\quad \\mathrm{mkHom}(m_1,s_1)\\cdot \\mathrm{mkHom}(m_2,s_2)=\\mathrm{mkHom}(m_1m_2,s_1s_2).$$$
Lean4
/-- `Localization.mk` as a monoid hom. -/
@[to_additive (attr := simps) /-- `Localization.mk` as a monoid hom. -/
]
def mkHom : M × S →* Localization S where
toFun x := mk x.1 x.2
map_one' := mk_one
map_mul' _ _ := (mk_mul ..).symm
