mapEquiv — Mathlib

English

If h is a monoid isomorphism, then there is a corresponding isomorphism of unit groups mapEquiv h: Mˣ ≃* Nˣ.

Русский

Пусть h — изоморфизм моноидов; существует соответствующий изоморфизм групп единиц mapEquiv h: Mˣ ≃* Nˣ.

LaTeX

$$$\\mathrm{mapEquiv}(h): M^{\\times} \\simeq N^{\\times}$$$

Lean4

/-- A multiplicative equivalence of monoids defines a multiplicative equivalence
of their groups of units. -/
def mapEquiv (h : M ≃* N) : Mˣ ≃* Nˣ :=
  { map h.toMonoidHom with invFun := map h.symm.toMonoidHom, left_inv := fun u => ext <| h.left_inv u,
    right_inv := fun u => ext <| h.right_inv u }

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