toSubgroup' — Mathlib

English

There is an order isomorphism between AddSubgroup(Additive G) and Subgroup(G), which is the inverse of the previous correspondence.

Русский

Существует обратное упорядоченное соответствие между AddSubgroup(Additive G) и Subgroup(G), являющееся обратным к предыдущему соответствию.

LaTeX

$$$$ \\mathrm{AddSubgroup}(\\mathrm{Additive}~G) \\cong_o \\mathrm{Subgroup}(G). $$$$

Lean4

/-- Additive subgroup of an additive group `Additive G` are isomorphic to subgroup of `G`. -/
abbrev toSubgroup' : AddSubgroup (Additive G) ≃o Subgroup G :=
  Subgroup.toAddSubgroup.symm

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