English
The isomorphism between ZMod n and any cyclic additive group of cardinality n exists given the cyclic structure; more precisely, there is a canonical Additive Isom between ZMod n and any cyclic group of order n.
Русский
Существует указующее изоморфное отображение между ZMod n и любой цикличной аддитивной группой порядком n.
LaTeX
$$$\exists\, \phi: \mathbb{Z}/n\mathbb{Z} \cong^+ G \quad (|G|=n,\ G\text{ cyclic})$$$
Lean4
/-- The isomorphism from `ZMod n` to any cyclic additive group of `Nat.card` equal to `n`. -/
noncomputable def zmodAddCyclicAddEquiv [AddGroup G] (h : IsAddCyclic G) : ZMod (Nat.card G) ≃+ G :=
by
let n := Nat.card G
let ⟨g, surj⟩ := Classical.indefiniteDescription _ h.exists_generator
have kereq : ((zmultiplesHom G) g).ker = zmultiples ↑(Nat.card G) :=
by
rw [zmultiplesHom_ker_eq]
congr
rw [← Nat.card_zmultiples]
exact Nat.card_congr (Equiv.subtypeUnivEquiv surj)
exact
Int.quotientZMultiplesNatEquivZMod n |>.symm.trans <|
QuotientAddGroup.quotientAddEquivOfEq kereq |>.symm.trans <|
QuotientAddGroup.quotientKerEquivOfSurjective (zmultiplesHom G g) surj
