English
Let G be a finite cyclic subgroup of the units K^×. For k > 0, if k < |G|, then the sum over G of x^k is zero: ∑_{x∈G} x^k = 0.
Русский
Пусть G — конечная циклическая подгруппа единиц K^×. Если k > 0 и k < |G|, то сумма x^k по x∈G равна нулю: ∑_{x∈G} x^k = 0.
LaTeX
$$$\sum_{x \in G} x^k = 0$$$
Lean4
@[simp]
theorem sum_subgroup_pow_eq_zero [CommRing K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] {k : ℕ} (k_pos : k ≠ 0)
(k_lt_card_G : k < Fintype.card G) : ∑ x : G, ((x : Kˣ) : K) ^ k = 0 :=
by
rw [← Nat.card_eq_fintype_card] at k_lt_card_G
nontriviality K
have := NoZeroDivisors.to_isDomain K
rcases (exists_pow_ne_one_of_isCyclic k_pos k_lt_card_G) with ⟨a, ha⟩
rw [Finset.sum_eq_multiset_sum]
have h_multiset_map :
Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k) =
Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) :=
by
simp_rw [← mul_pow]
have as_comp :
(fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k) =
(fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a :=
by
funext x
simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]
rw [as_comp, ← Multiset.map_map]
congr
rw [eq_comm]
exact Multiset.map_univ_val_equiv (Equiv.mulRight a)
have h_multiset_map_sum :
(Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k) Finset.univ.val).sum =
(Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) Finset.univ.val).sum :=
by rw [h_multiset_map]
rw [Multiset.sum_map_mul_right] at h_multiset_map_sum
have hzero : (((a : Kˣ) : K) ^ k - 1 : K) * (Multiset.map (fun i : G => (i.val : K) ^ k) Finset.univ.val).sum = 0 :=
by rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
rw [mul_eq_zero] at hzero
refine hzero.resolve_left fun h => ha ?_
ext
rw [← sub_eq_zero]
simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, Units.val_one, h]
