toAddSubgroup' — Mathlib

English

There is an order isomorphism from Subgroup(Multiplicative A) to AddSubgroup A, the inverse of the previous correspondence.

Русский

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

LaTeX

$$$$ \\mathrm{Subgroup}(\\mathrm{Multiplicative}~A) \\cong_o \\mathrm{AddSubgroup}~A. $$$$

Lean4

/-- Subgroups of an additive group `Multiplicative A` are isomorphic to additive subgroups of `A`.
-/
abbrev toAddSubgroup' : Subgroup (Multiplicative A) ≃o AddSubgroup A :=
  AddSubgroup.toSubgroup.symm

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