mk_eq_monoidOf_mk'_apply — Mathlib

English

The mk' construction lifts to the localization, maintaining consistency with mk on the base monoid.

Русский

Конструкция mk' восстанавливает локализацию, сохраняя согласованность с mk на базовом моноиде.

LaTeX

$$$mk'_\text{eq}$$$

Lean4

@[to_additive]
theorem mk_eq_monoidOf_mk'_apply (x y) : mk x y = (monoidOf S).mk' x y :=
  show _ = _ * _ from
    (Submonoid.LocalizationMap.mul_inv_right (monoidOf S).map_units _ _ _).2 <|
      by
      dsimp
      rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
      conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
      exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

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