Theorems · Definition · group theory

mulEquivOfPrimeCardEq

{G : Type u_2} →
  {G' : Type u_3} →
    {p : ℕ} → [inst : Group G] → [inst_1 : Group G'] → [Fact (Nat.Prime p)] → Nat.card G = p → Nat.card G' = p → G ≃* G'

Two groups of the same prime cardinality are isomorphic.

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupFact