English
Let R be a domain. For any n > 0 and a ∈ R, the polynomial X^n − a has at most n roots in R (counted with multiplicity).
Русский
Пусть R — областьность. Для любого n > 0 и a ∈ R многочлон X^n − a имеет не более n корней в R с учётом кратностей.
LaTeX
$$$0 < n \Rightarrow \#\operatorname{roots}\left(X^{n} - C a\right) \le n$$$
Lean4
theorem card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) : Multiset.card (roots ((X : R[X]) ^ n - C a)) ≤ n :=
WithBot.coe_le_coe.1 <|
calc
(Multiset.card (roots ((X : R[X]) ^ n - C a)) : WithBot ℕ) ≤ degree ((X : R[X]) ^ n - C a) :=
card_roots (X_pow_sub_C_ne_zero hn a)
_ = n := degree_X_pow_sub_C hn a