card_zpowers — Mathlib

English

The size of the set of z-powers equals the order of a: |zpowers(a)| = ord(a).

Русский

Размер множества z-производных равно порядку элемента: |zpowers(a)| = ord(a).

LaTeX

$$$ |\mathrm{zpowers}(a)| = \operatorname{ord}(a) $$$

Lean4

/-- See also `Fintype.card_zpowers`. -/
@[to_additive (attr := simp) /-- See also `Fintype.card_zmultiples`. -/
    ]
theorem card_zpowers : Nat.card (zpowers a) = orderOf a :=
  by
  have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))
  rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this

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