card_zpowers — Mathlib

English

For a finite group G, the number of elements in zpowers x equals orderOf x.

Русский

Для конечной группы G число элементов zpowers x равно orderOf x.

LaTeX

$$Fintype.card (zpowers x) = orderOf x$$

Lean4

/-- See also `Nat.card_zpowers`. -/
@[to_additive /-- See also `Nat.card_zmultiples`. -/
    ]
theorem card_zpowers : Fintype.card (zpowers x) = orderOf x :=
  (Fintype.card_eq.2 ⟨finEquivZPowers <| isOfFinOrder_of_finite _⟩).symm.trans <| Fintype.card_fin (orderOf x)

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