image_range_card — Mathlib

English

If every element is a power of a, then the image of i ↦ a^i for i in 0..card α - 1 equals the whole group.

Русский

Если каждый элемент является степенью a, то образ функции i ↦ a^i на i=0..card α-1 равен всей группе.

LaTeX

$$Finset.image (fun i => a^i) (range (Nat.card α)) = univ$$

Lean4

@[to_additive]
theorem image_range_card (ha : ∀ x : α, x ∈ zpowers a) : Finset.image (fun i => a ^ i) (range (Nat.card α)) = univ := by
  rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]

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