groupIsoToMulEquiv — Mathlib

English

An isomorphism in GrpCat gives a MulEquiv between the underlying groups.

Русский

Изоморфизм в GrpCat задаёт MulEquiv между базовыми группами.

LaTeX

$$$$ \forall X,Y:\mathrm{GrpCat},\; i: X \cong Y \Rightarrow X \simeq_* Y. $$$$

Lean4

/-- Build a `MulEquiv` from an isomorphism in the category `GrpCat`. -/
@[to_additive (attr := simp)]
def groupIsoToMulEquiv {X Y : GrpCat} (i : X ≅ Y) : X ≃* Y :=
  MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp)

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