card_submonoidPowers — Mathlib

English

The cardinality of powers a equals orderOf a (with orderOf a = 0 for infinite order).

Русский

Кардиналность множества степеней a равна orderOf(a) (при бесконечном порядке orderOf(a) = 0).

LaTeX

$$\operatorname{card}(\mathrm{powers}(a)) = \operatorname{orderOf}(a)$$

Lean4

/-- See also `orderOf_eq_card_powers`. -/
@[to_additive /-- See also `addOrder_eq_card_multiples`. -/
    ]
theorem card_submonoidPowers : Nat.card (powers a) = orderOf a := by
  classical
  by_cases ha : IsOfFinOrder a
  · exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp
  · have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

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