iff_exponent_eq_card — Mathlib

English

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

Русский

Для конечной коммутативной группы верно: IsCyclic α тогда и только тогда, когда exp α = |α|.

LaTeX

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

Lean4

@[to_additive]
theorem iff_exponent_eq_card [CommGroup α] [Finite α] : IsCyclic α ↔ exponent α = Nat.card α :=
  ⟨fun _ => IsCyclic.exponent_eq_card, IsCyclic.of_exponent_eq_card⟩

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