addEquivOfAddCyclicCardEq — Mathlib

English

Two cyclic groups of the same order are isomorphic.

Русский

Две циклические группы одинакового порядка изоморфны.

LaTeX

$$$G \cong^* G' \text{ if } |G|=|G'|$ and both cyclic$$

Lean4

/-- Two cyclic additive groups of the same cardinality are isomorphic. -/
noncomputable def addEquivOfAddCyclicCardEq [AddGroup G] [AddGroup G'] [hG : IsAddCyclic G] [hH : IsAddCyclic G']
    (hcard : Nat.card G = Nat.card G') : G ≃+ G' :=
  hcard ▸ zmodAddCyclicAddEquiv hG |>.symm.trans (zmodAddCyclicAddEquiv hH)

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