is_simple_iff_isCyclic_and_prime_card

English

For finite commutative groups, IsCyclic α holds iff exponent α = card α.

Русский

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

LaTeX

$$IsCyclic α ↔ exponent α = Nat.card α$$

Lean4

@[to_additive]
theorem is_simple_iff_isCyclic_and_prime_card [Finite α] [CommGroup α] :
    IsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime :=
  by
  constructor
  · intro h
    exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩
  · rintro ⟨_, hp⟩
    haveI : Fact (Nat.card α).Prime := ⟨hp⟩
    exact isSimpleGroup_of_prime_card rfl

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