English
Let G be a finite group and S ⊆ G. For any k with k ≥ |G|, the number of products of k elements from S equals the number of products of |G| elements from S.
Русский
Пусть G конечной группы; S ⊆ G. Для любого k ≥ |G| число элементов, получаемых как произведение k элементов из S, равно числу элементов, получаемых как произведение |G| элементов из S.
LaTeX
$$$|S^{k}| = |S^{|G|}| \\quad\\text{whenever } |G| \\le k$$$
Lean4
@[to_additive]
theorem card_pow_eq_card_pow_card_univ [∀ k : ℕ, DecidablePred (· ∈ S ^ k)] :
∀ k, Fintype.card G ≤ k → Fintype.card (↥(S ^ k)) = Fintype.card (↥(S ^ Fintype.card G)) :=
by
have hG : 0 < Fintype.card G := Fintype.card_pos
rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)
· refine fun k hk ↦ Fintype.card_congr ?_
rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]
have key :
∀ (a) (s t : Set G) [Fintype s] [Fintype t], (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t :=
by
refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))
have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha
refine fun _ ↦
Nat.stabilises_of_monotone mono (fun n ↦ set_fintype_card_le_univ (S ^ n)) fun n h ↦
le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) ?_)
replace h₂ : S ^ n * { a } = S ^ (n + 1) :=
by
have : Fintype (S ^ n * Set.singleton a) := by classical apply fintypeMul
refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
· exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)
· convert key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)
rw [pow_succ', ← h₂, ← mul_assoc, ← pow_succ', h₂, mul_singleton, forall_mem_image]
intro x hx
rwa [mul_inv_cancel_right]
