English
If hζ asserts that ζ is a primitive n-th root of unity and α^n = a, then the set of n-th roots of a is exactly the multiset consisting of α multiplied by powers of ζ, i.e., { α, ζα, ζ^2α, ..., ζ^{n-1}α } counted with multiplicities.
Русский
Пусть ζ — примитивный корень порядка n, и α^n = a. Тогда множество корней степени n у числа a равно мультинадному множеству { α, ζα, ζ^2α, ..., ζ^{n-1}α }.
LaTeX
$$$\\operatorname{nthRoots}(n,a) = (\\operatorname{Multiset.range}(n)).map (\\lambda i, \\zeta^i \\cdot \\alpha)$$$
Lean4
theorem nthRoots_eq {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α a : R} (e : α ^ n = a) :
nthRoots n a = (Multiset.range n).map (ζ ^ · * α) :=
by
obtain (rfl | hn) := n.eq_zero_or_pos; · simp
by_cases hα : α = 0
· rw [hα, zero_pow hn.ne'] at e
simp only [hα, e.symm, nthRoots_zero_right, mul_zero, Multiset.map_const', Multiset.card_range]
classical
symm; apply Multiset.eq_of_le_of_card_le
· rw [← Finset.range_val, ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]
intro x hx
simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map, Multiset.mem_range] at hx
obtain ⟨m, _, rfl⟩ := hx
rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_mul]
· simpa only [Multiset.card_map, Multiset.card_range] using card_nthRoots n a
