English
Let hζ be a primitive n-th root of unity. Then for any a, the number of nth roots of a is n if a is an n-th power (i.e., ∃ α with α^n = a), and 0 otherwise.
Русский
Пусть hζ — примитивный корень n-й степени единицы. Тогда для любого a число корней степени n равно n, если существует α с α^n = a, иначе равно 0.
LaTeX
$$$\\operatorname{card}(\\operatorname{nthRoots}(n,a)) = \\begin{cases} n, & \\exists α, α^n = a \\\\ 0, & \\text{иначе} \\end{cases}$$$
Lean4
theorem card_nthRoots {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) (a : R) :
Multiset.card (nthRoots n a) = if ∃ α, α ^ n = a then n else 0 :=
by
split_ifs with h
· obtain ⟨α, hα⟩ := h
rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]
· obtain (rfl | hn) := n.eq_zero_or_pos; · simp
push_neg at h
simpa only [Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_notMem, mem_nthRoots hn]
