card_roots_X_pow_sub_C — Mathlib

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

Похожие утверждения