mulEquivOfPrimeCardEq — Mathlib

English

Two groups of the same prime order p are isomorphic.

Русский

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

LaTeX

$$$\text{Card}(G)=\text{Card}(G')=p\ \Rightarrow\ G \cong^* G'$$$

Lean4

/-- Two groups of the same prime cardinality are isomorphic. -/
@[to_additive /-- Two additive groups of the same prime cardinality are isomorphic. -/
    ]
noncomputable def mulEquivOfPrimeCardEq {p : ℕ} [Group G] [Group G'] [Fact p.Prime] (hG : Nat.card G = p)
    (hH : Nat.card G' = p) : G ≃* G' := by
  have hGcyc := isCyclic_of_prime_card hG
  have hHcyc := isCyclic_of_prime_card hH
  apply mulEquivOfCyclicCardEq
  exact hG.trans hH.symm

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