map_comap_eq — Mathlib

English

The companion lemmas establish the explicit construction and properties of the equivalence between Units M and IsUnit.submonoid M.

Русский

Леммы задают явное построение и свойства эквивалентности между Units M и IsUnit.submonoid M.

LaTeX

$$$ Units(M) \equiv IsUnit.submonoid M $ with explicit maps and inverse$$

Lean4

@[to_additive]
theorem map_comap_eq (f : F) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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