mulEquivOfCyclicCardEq — Mathlib

English

Two cyclic additive groups of the same cardinality are isomorphic.

Русский

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

LaTeX

$$$\forall G,G'\, (\text{IsAddCyclic}(G) \land \text{IsAddCyclic}(G') \land |G|=|G'|) \Rightarrow G \cong^+ G'$$$

Lean4

/-- Two cyclic groups of the same cardinality are isomorphic. -/
@[to_additive existing]
noncomputable def mulEquivOfCyclicCardEq [Group G] [Group G'] [hG : IsCyclic G] [hH : IsCyclic G']
    (hcard : Nat.card G = Nat.card G') : G ≃* G' :=
  hcard ▸ zmodCyclicMulEquiv hG |>.symm.trans (zmodCyclicMulEquiv hH)

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