English
Under decidable equality, the image of i ↦ x^i on range(orderOf x) equals the subgroup of powers of x.
Русский
При k ясного равенства образ i ↦ x^i на диапазоне orderOf x совпадает с подгруппой степеней x.
LaTeX
$$Finset.image (\u2061i => x^i) (Finset.range (orderOf x)) = (zpowers x).toFinset$$
Lean4
/-- A nonempty idempotent subset of a finite group is a subgroup -/
@[to_additive /-- A nonempty idempotent subset of a finite additive group is a subgroup -/
]
def subgroupOfIdempotent {G : Type*} [Group G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S * S = S) :
Subgroup G :=
{ submonoidOfIdempotent S hS1 hS2 with
carrier := S
inv_mem' := fun {a} ha =>
show a⁻¹ ∈ submonoidOfIdempotent S hS1 hS2
by
rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]
exact pow_mem ha (orderOf a - 1) }
