ofMulEquivOfDom_id — Mathlib

English

A special case of the dom-compatibility when the isomorphism is the identity; the induced localization map equals the original one.

Русский

Особый случай совместимости домена, когда изоморфизм является тождественным; полученная локализационная карта равна исходной.

LaTeX

$$$f.ofMulEquivOfDom(H_{\mathrm{id}}) = f$, где $H_{\mathrm{id}}$ соответствует тождественному отображению.$$

Lean4

/-- A special case of `f ∘ id = f`, `f` a Localization map. -/
@[to_additive (attr := simp) /-- A special case of `f ∘ id = f`, `f` a Localization map. -/
    ]
theorem ofMulEquivOfDom_id :
    f.ofMulEquivOfDom
        (show S.map (MulEquiv.refl M).toMonoidHom = S from
          Submonoid.ext fun x ↦ ⟨fun ⟨_, hy, h⟩ ↦ h ▸ hy, fun h ↦ ⟨x, h, rfl⟩⟩) =
      f :=
  by ext; rfl

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