Mathlib.Algebra.Polynomial.Roots

Polynomial.roots definition

(p : R[X]) : Multiset R

Full source

/-- `roots p` noncomputably gives a multiset containing all the roots of `p`,
including their multiplicities. -/
noncomputable def roots (p : R[X]) : Multiset R :=
  haveI := Classical.decEq R
  haveI := Classical.dec (p = 0)
  if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h)

Multiset of roots of a polynomial (with multiplicities)

Informal description

For a polynomial $ p $ over a commutative ring $ R $, the multiset `roots p` contains all roots of $ p $ with their multiplicities. If $ p = 0 $, the multiset is empty. The definition is noncomputable and uses classical logic to choose a suitable multiset when $ p \neq 0 $.

Polynomial.roots_def theorem

 [DecidableEq R] (p : R[X]) [Decidable (p = 0)] :
  p.roots = if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h)

Full source

theorem roots_def [DecidableEq R] (p : R[X]) [Decidable (p = 0)] :
    p.roots = if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h) := by
  rename_i iR ip0
  obtain rfl := Subsingleton.elim iR (Classical.decEq R)
  obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))
  rfl

Definition of Polynomial Roots Multiset via Axiom of Choice

Informal description

For a polynomial $p$ over a commutative ring $R$ with decidable equality, the multiset of roots $\text{roots}(p)$ is defined as follows: - If $p = 0$, then $\text{roots}(p) = \emptyset$. - Otherwise, $\text{roots}(p)$ is the multiset chosen by the axiom of choice from the existence proof provided by `exists_multiset_roots`.

Polynomial.roots_zero theorem

: (0 : R[X]).roots = 0

Full source

@[simp]
theorem roots_zero : (0 : R[X]).roots = 0 :=
  dif_pos rfl

Roots of the Zero Polynomial are Empty

Informal description

The multiset of roots of the zero polynomial is empty, i.e., $\text{roots}(0) = \emptyset$.

Polynomial.card_roots theorem

(hp0 : p ≠ 0) : (Multiset.card (roots p) : WithBot ℕ) ≤ degree p

Full source

theorem card_roots (hp0 : p ≠ 0) : (Multiset.card (roots p) : WithBot ℕ) ≤ degree p := by
  classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1

Upper Bound on Number of Roots of a Polynomial: $|\text{roots}(p)| \leq \deg p$

Informal description

For any nonzero polynomial $p$ over a commutative ring $R$, the cardinality of the multiset of roots of $p$ (counted with multiplicities) is at most the degree of $p$. In other words, if $\text{roots}(p)$ denotes the multiset of roots of $p$, then $|\text{roots}(p)| \leq \deg p$.

Polynomial.card_roots' theorem

(p : R[X]) : Multiset.card p.roots ≤ natDegree p

Full source

theorem card_roots' (p : R[X]) : Multiset.card p.roots ≤ natDegree p := by
  by_cases hp0 : p = 0
  · simp [hp0]
  exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

Upper Bound on Number of Roots of a Polynomial: $|\text{roots}(p)| \leq \deg p$

Informal description

For any polynomial $p$ over a commutative ring $R$, the number of roots of $p$ (counted with multiplicities) is at most the degree of $p$. In other words, if $\text{roots}(p)$ denotes the multiset of roots of $p$, then $|\text{roots}(p)| \leq \deg p$.

Polynomial.card_roots_sub_C theorem

{p : R[X]} {a : R} (hp0 : 0 < degree p) : (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree p

Full source

theorem card_roots_sub_C {p : R[X]} {a : R} (hp0 : 0 < degree p) :
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree p :=
  calc
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree (p - C a) :=
      card_roots <| mt sub_eq_zero.1 fun h => not_le_of_gt hp0 <| h.symm ▸ degree_C_le
    _ = degree p := by rw [sub_eq_add_neg, ← C_neg]; exact degree_add_C hp0

Upper Bound on Roots of Shifted Polynomial: $|\text{roots}(p - a)| \leq \deg p$

Informal description

For any polynomial $p$ over a commutative ring $R$ with positive degree, and for any element $a \in R$, the cardinality of the multiset of roots of $p - a$ (counted with multiplicities) is at most the degree of $p$. In other words, $|\text{roots}(p - a)| \leq \deg p$.

Polynomial.card_roots_sub_C' theorem

{p : R[X]} {a : R} (hp0 : 0 < degree p) : Multiset.card (p - C a).roots ≤ natDegree p

Full source

theorem card_roots_sub_C' {p : R[X]} {a : R} (hp0 : 0 < degree p) :
    Multiset.card (p - C a).roots ≤ natDegree p :=
  WithBot.coe_le_coe.1
    (le_trans (card_roots_sub_C hp0)
      (le_of_eq <| degree_eq_natDegree fun h => by simp_all [lt_irrefl]))

Upper Bound on Roots of Shifted Polynomial: $|\mathrm{roots}(p - a)| \leq \deg p$

Informal description

For any polynomial $p$ over a commutative ring $R$ with positive degree and any element $a \in R$, the number of roots (counted with multiplicities) of the polynomial $p - a$ is at most the degree of $p$. That is, \[ |\mathrm{roots}(p - a)| \leq \deg p. \]

Polynomial.count_roots theorem

[DecidableEq R] (p : R[X]) : p.roots.count a = rootMultiplicity a p

Full source

@[simp]
theorem count_roots [DecidableEq R] (p : R[X]) : p.roots.count a = rootMultiplicity a p := by
  classical
  by_cases hp : p = 0
  · simp [hp]
  rw [roots_def, dif_neg hp]
  exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

Root Multiplicity Equals Count in Roots Multiset

Informal description

For a polynomial $p$ over a commutative ring $R$ with decidable equality, the multiplicity of an element $a \in R$ in the multiset of roots of $p$ equals the root multiplicity of $a$ in $p$. That is, $\mathrm{count}(a, \mathrm{roots}(p)) = \mathrm{rootMultiplicity}(a, p)$.

Polynomial.mem_roots' theorem

: a ∈ p.roots ↔ p ≠ 0 ∧ IsRoot p a

Full source

@[simp]
theorem mem_roots' : a ∈ p.rootsa ∈ p.roots ↔ p ≠ 0 ∧ IsRoot p a := by
  classical
  rw [← count_pos, count_roots p, rootMultiplicity_pos']

Characterization of Polynomial Root Membership: $a \in \mathrm{roots}(p) \iff (p \neq 0 \text{ and } p(a) = 0)$

Informal description

For a polynomial $p$ over a commutative ring $R$ and an element $a \in R$, the element $a$ belongs to the multiset of roots of $p$ if and only if $p$ is nonzero and $a$ is a root of $p$. In other words: \[ a \in \mathrm{roots}(p) \iff (p \neq 0 \text{ and } p(a) = 0). \]

Polynomial.mem_roots theorem

(hp : p ≠ 0) : a ∈ p.roots ↔ IsRoot p a

Full source

theorem mem_roots (hp : p ≠ 0) : a ∈ p.rootsa ∈ p.roots ↔ IsRoot p a :=
  mem_roots'.trans <| and_iff_right hp

Characterization of Root Membership for Nonzero Polynomials

Informal description

For a nonzero polynomial $p$ over a commutative ring $R$, an element $a \in R$ is in the multiset of roots of $p$ if and only if $a$ is a root of $p$. That is, \[ a \in \mathrm{roots}(p) \iff p(a) = 0. \]

Polynomial.ne_zero_of_mem_roots theorem

(h : a ∈ p.roots) : p ≠ 0

Full source

theorem ne_zero_of_mem_roots (h : a ∈ p.roots) : p ≠ 0 :=
  (mem_roots'.1 h).1

Nonzero Polynomial Condition for Root Membership

Informal description

If an element $a$ belongs to the multiset of roots of a polynomial $p$, then $p$ is not the zero polynomial.

Polynomial.isRoot_of_mem_roots theorem

(h : a ∈ p.roots) : IsRoot p a

Full source

theorem isRoot_of_mem_roots (h : a ∈ p.roots) : IsRoot p a :=
  (mem_roots'.1 h).2

Root Membership Implies Root Condition

Informal description

For any polynomial $p$ over a commutative ring $R$ and any element $a \in R$, if $a$ is a root of $p$ (i.e., $a$ appears in the multiset of roots of $p$), then $p(a) = 0$.

Polynomial.mem_roots_map_of_injective theorem

 [Semiring S] {p : S[X]} {f : S →+* R} (hf : Function.Injective f) {x : R} (hp : p ≠ 0) :
  x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

Full source

theorem mem_roots_map_of_injective [Semiring S] {p : S[X]} {f : S →+* R}
    (hf : Function.Injective f) {x : R} (hp : p ≠ 0) : x ∈ (p.map f).rootsx ∈ (p.map f).roots ↔ p.eval₂ f x = 0 := by
  rw [mem_roots ((Polynomial.map_ne_zero_iff hf).mpr hp), IsRoot, eval_map]

Root Preservation under Injective Polynomial Mapping: $x \in \text{roots}(p.map\ f) \leftrightarrow \text{eval}_2\ f\ x\ p = 0$

Informal description

Let $S$ and $R$ be semirings, $p \neq 0$ a polynomial over $S$, and $f : S \to R$ an injective ring homomorphism. For any $x \in R$, the element $x$ is a root of the polynomial $p$ mapped via $f$ (i.e., $x \in \text{roots}(p.map\ f)$) if and only if the evaluation of $p$ at $x$ via $f$ is zero (i.e., $p.eval₂\ f\ x = 0$).

Polynomial.mem_roots_iff_aeval_eq_zero theorem

{x : R} (w : p ≠ 0) : x ∈ roots p ↔ aeval x p = 0

Full source

lemma mem_roots_iff_aeval_eq_zero {x : R} (w : p ≠ 0) : x ∈ roots px ∈ roots p ↔ aeval x p = 0 := by
  rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w,
    Algebra.id.map_eq_id, map_id]

Characterization of Roots via Algebra Homomorphism Evaluation: $x \in \text{roots}(p) \leftrightarrow \text{aeval}_x(p) = 0$

Informal description

For any nonzero polynomial $p$ over a commutative ring $R$ and any element $x \in R$, $x$ is a root of $p$ (i.e., $x$ appears in the multiset of roots of $p$) if and only if the evaluation of $p$ at $x$ via the algebra homomorphism $\text{aeval}_x$ is zero, i.e., $\text{aeval}_x(p) = 0$.

Polynomial.card_le_degree_of_subset_roots theorem

{p : R[X]} {Z : Finset R} (h : Z.val ⊆ p.roots) : #Z ≤ p.natDegree

Full source

theorem card_le_degree_of_subset_roots {p : R[X]} {Z : Finset R} (h : Z.val ⊆ p.roots) :
    #Z ≤ p.natDegree :=
  (Multiset.card_le_card (Finset.val_le_iff_val_subset.2 h)).trans (Polynomial.card_roots' p)

Finite Subset of Roots Has Cardinality Bounded by Degree: $|Z| \leq \deg p$

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a nonzero polynomial. For any finite subset $Z \subseteq R$ such that every element of $Z$ is a root of $p$ (i.e., $Z \subseteq \text{roots}(p)$), the cardinality of $Z$ is at most the degree of $p$. In other words, $|Z| \leq \deg p$.

Polynomial.finite_setOf_isRoot theorem

{p : R[X]} (hp : p ≠ 0) : Set.Finite {x | IsRoot p x}

Full source

theorem finite_setOf_isRoot {p : R[X]} (hp : p ≠ 0) : Set.Finite { x | IsRoot p x } := by
  classical
  simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
    using p.roots.toFinset.finite_toSet

Finiteness of the Root Set of a Nonzero Polynomial

Informal description

For any nonzero polynomial $p$ over a commutative ring $R$, the set of roots $\{x \in R \mid p(x) = 0\}$ is finite.

Polynomial.exists_max_root theorem

[LinearOrder R] (p : R[X]) (hp : p ≠ 0) : ∃ x₀, ∀ x, p.IsRoot x → x ≤ x₀

Full source

theorem exists_max_root [LinearOrder R] (p : R[X]) (hp : p ≠ 0) : ∃ x₀, ∀ x, p.IsRoot x → x ≤ x₀ :=
  Set.exists_upper_bound_image _ _ <| finite_setOf_isRoot hp

Existence of Maximal Root for Nonzero Polynomials over Linearly Ordered Rings

Informal description

Let $R$ be a linearly ordered commutative ring and $p \in R[X]$ be a nonzero polynomial. Then there exists a maximal root $x_0 \in R$ of $p$, meaning that for every root $x$ of $p$, we have $x \leq x_0$.

Polynomial.exists_min_root theorem

[LinearOrder R] (p : R[X]) (hp : p ≠ 0) : ∃ x₀, ∀ x, p.IsRoot x → x₀ ≤ x

Full source

theorem exists_min_root [LinearOrder R] (p : R[X]) (hp : p ≠ 0) : ∃ x₀, ∀ x, p.IsRoot x → x₀ ≤ x :=
  Set.exists_lower_bound_image _ _ <| finite_setOf_isRoot hp

Existence of Minimal Root for Nonzero Polynomials over Linearly Ordered Rings

Informal description

Let $R$ be a linearly ordered commutative ring and $p \in R[X]$ be a nonzero polynomial. Then there exists a minimal root $x_0$ of $p$ such that for every root $x$ of $p$, we have $x_0 \leq x$.

Polynomial.roots_mul theorem

{p q : R[X]} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots

Full source

theorem roots_mul {p q : R[X]} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots := by
  classical
  exact Multiset.ext.mpr fun r => by
    rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

Root Multiset Additivity under Polynomial Multiplication: $\mathrm{roots}(p \cdot q) = \mathrm{roots}(p) + \mathrm{roots}(q)$

Informal description

Let $R$ be a commutative ring and let $p, q \in R[X]$ be nonzero polynomials. Then the multiset of roots (with multiplicities) of the product $p \cdot q$ is equal to the sum of the multisets of roots of $p$ and $q$, i.e., \[ \mathrm{roots}(p \cdot q) = \mathrm{roots}(p) + \mathrm{roots}(q). \]

Polynomial.roots.le_of_dvd theorem

(h : q ≠ 0) : p ∣ q → roots p ≤ roots q

Full source

theorem roots.le_of_dvd (h : q ≠ 0) : p ∣ q → roots p ≤ roots q := by
  rintro ⟨k, rfl⟩
  exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

Root Multiset Subset under Divisibility: $\mathrm{roots}(p) \leq \mathrm{roots}(q)$ when $p \mid q$

Informal description

Let $R$ be a commutative ring and let $p, q \in R[X]$ be polynomials with $q \neq 0$. If $p$ divides $q$, then the multiset of roots of $p$ (with multiplicities) is a submultiset of the multiset of roots of $q$, i.e., \[ \mathrm{roots}(p) \leq \mathrm{roots}(q). \]

Polynomial.mem_roots_sub_C' theorem

{p : R[X]} {a x : R} : x ∈ (p - C a).roots ↔ p ≠ C a ∧ p.eval x = a

Full source

theorem mem_roots_sub_C' {p : R[X]} {a x : R} : x ∈ (p - C a).rootsx ∈ (p - C a).roots ↔ p ≠ C a ∧ p.eval x = a := by
  rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]

Root Membership Criterion for Shifted Polynomial: $x \in \mathrm{roots}(p - a) \iff (p \neq a \text{ and } p(x) = a)$

Informal description

For a polynomial $p$ over a commutative ring $R$ and elements $a, x \in R$, the element $x$ belongs to the multiset of roots of the polynomial $p - a$ if and only if $p$ is not the constant polynomial $a$ and $x$ is a root of $p - a$ (i.e., $p(x) = a$). In other words: \[ x \in \mathrm{roots}(p - a) \iff (p \neq a \text{ and } p(x) = a). \]

Polynomial.mem_roots_sub_C theorem

{p : R[X]} {a x : R} (hp0 : 0 < degree p) : x ∈ (p - C a).roots ↔ p.eval x = a

Full source

theorem mem_roots_sub_C {p : R[X]} {a x : R} (hp0 : 0 < degree p) :
    x ∈ (p - C a).rootsx ∈ (p - C a).roots ↔ p.eval x = a :=
  mem_roots_sub_C'.trans <| and_iff_right fun hp => hp0.not_le <| hp.symm ▸ degree_C_le

Root membership criterion for shifted polynomial with positive degree

Informal description

For a polynomial $p$ over a commutative ring $R$ with $\deg(p) > 0$, and for any elements $a, x \in R$, the element $x$ belongs to the multiset of roots of the polynomial $p - a$ if and only if $x$ is a root of $p - a$, i.e., $p(x) = a$. In other words: \[ x \in \mathrm{roots}(p - a) \iff p(x) = a. \]

Polynomial.roots_X_sub_C theorem

(r : R) : roots (X - C r) = { r }

Full source

@[simp]
theorem roots_X_sub_C (r : R) : roots (X - C r) = {r} := by
  classical
  ext s
  rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

Roots of Linear Polynomial: $\mathrm{roots}(X - r) = \{r\}$

Informal description

For any element $r$ in a commutative ring $R$, the multiset of roots of the polynomial $X - r$ is the singleton multiset $\{r\}$.

Polynomial.roots_X_add_C theorem

(r : R) : roots (X + C r) = {-r}

Full source

@[simp]
theorem roots_X_add_C (r : R) : roots (X + C r) = {-r} := by simpa using roots_X_sub_C (-r)

Roots of Linear Polynomial: $\mathrm{roots}(X + r) = \{-r\}$

Informal description

For any element $r$ in a commutative ring $R$, the multiset of roots of the polynomial $X + r$ is the singleton multiset $\{-r\}$.

Polynomial.roots_X theorem

: roots (X : R[X]) = {0}

Full source

@[simp]
theorem roots_X : roots (X : R[X]) = {0} := by rw [← roots_X_sub_C, C_0, sub_zero]

Roots of the Polynomial $X$: $\mathrm{roots}(X) = \{0\}$

Informal description

For any commutative ring $R$, the multiset of roots of the polynomial $X$ in $R[X]$ is the singleton multiset $\{0\}$.

Polynomial.roots_C theorem

(x : R) : (C x).roots = 0

Full source

@[simp]
theorem roots_C (x : R) : (C x).roots = 0 := by
  classical exact
  if H : x = 0 then by rw [H, C_0, roots_zero]
  else
    Multiset.ext.mpr fun r => (by
      rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)])

Constant Polynomial Has No Roots

Informal description

For any element $x$ in a commutative ring $R$, the multiset of roots of the constant polynomial $C(x)$ is empty, i.e., $\text{roots}(C(x)) = \emptyset$.

Polynomial.roots_one theorem

: (1 : R[X]).roots = ∅

Full source

@[simp]
theorem roots_one : (1 : R[X]).roots = ∅ :=
  roots_C 1

Roots of the Constant One Polynomial are Empty

Informal description

The multiset of roots of the constant polynomial $1$ in the polynomial ring $R[X]$ is empty, i.e., $\text{roots}(1) = \emptyset$.

Polynomial.roots_C_mul theorem

(p : R[X]) (ha : a ≠ 0) : (C a * p).roots = p.roots

Full source

@[simp]
theorem roots_C_mul (p : R[X]) (ha : a ≠ 0) : (C a * p).roots = p.roots := by
  by_cases hp : p = 0 <;>
    simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
      zero_add, mul_zero]

Root Multiset Invariance under Nonzero Scalar Multiplication: $\mathrm{roots}(a \cdot p) = \mathrm{roots}(p)$ for $a \neq 0$

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a polynomial. For any nonzero element $a \in R$, the multiset of roots (with multiplicities) of the polynomial $a \cdot p$ is equal to the multiset of roots of $p$, i.e., \[ \mathrm{roots}(a \cdot p) = \mathrm{roots}(p). \]

Polynomial.roots_smul_nonzero theorem

(p : R[X]) (ha : a ≠ 0) : (a • p).roots = p.roots

Full source

@[simp]
theorem roots_smul_nonzero (p : R[X]) (ha : a ≠ 0) : (a • p).roots = p.roots := by
  rw [smul_eq_C_mul, roots_C_mul _ ha]

Root Multiset Invariance under Nonzero Scalar Multiplication: $\text{roots}(a \cdot p) = \text{roots}(p)$ for $a \neq 0$

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ be a polynomial. For any nonzero element $a \in R$, the multiset of roots (with multiplicities) of the scalar multiple $a \cdot p$ is equal to the multiset of roots of $p$, i.e., \[ \text{roots}(a \cdot p) = \text{roots}(p). \]

Polynomial.roots_neg theorem

(p : R[X]) : (-p).roots = p.roots

Full source

@[simp]
lemma roots_neg (p : R[X]) : (-p).roots = p.roots := by
  rw [← neg_one_smul R p, roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)]

Root Multiset Invariance under Negation: $\text{roots}(-p) = \text{roots}(p)$

Informal description

For any polynomial $p$ over a commutative ring $R$, the multiset of roots (with multiplicities) of $-p$ is equal to the multiset of roots of $p$, i.e., \[ \text{roots}(-p) = \text{roots}(p). \]

Polynomial.roots_C_mul_X_sub_C_of_IsUnit theorem

(b : R) (a : Rˣ) : (C (a : R) * X - C b).roots = {a⁻¹ * b}

Full source

@[simp]
theorem roots_C_mul_X_sub_C_of_IsUnit (b : R) (a : Rˣ) : (C (a : R) * X - C b).roots =
    {a⁻¹ * b} := by
  rw [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
    Units.inv_mul, C_1, one_mul]
  exact roots_X_sub_C (a⁻¹ * b)

Roots of linear polynomial $aX - b$ when $a$ is a unit: $\mathrm{roots}(aX - b) = \{a^{-1}b\}$

Informal description

Let $R$ be a commutative ring and let $a$ be a unit in $R$. For any element $b \in R$, the multiset of roots of the linear polynomial $aX - b$ is the singleton $\{a^{-1}b\}$.

Polynomial.roots_C_mul_X_add_C_of_IsUnit theorem

(b : R) (a : Rˣ) : (C (a : R) * X + C b).roots = {-(a⁻¹ * b)}

Full source

@[simp]
theorem roots_C_mul_X_add_C_of_IsUnit (b : R) (a : Rˣ) : (C (a : R) * X + C b).roots =
    {-(a⁻¹ * b)} := by
  rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]

Roots of linear polynomial $aX + b$ when $a$ is a unit: $\mathrm{roots}(aX + b) = \{-a^{-1}b\}$

Informal description

Let $R$ be a commutative ring and let $a$ be a unit in $R$. For any element $b \in R$, the multiset of roots of the linear polynomial $aX + b$ is the singleton $\{-a^{-1}b\}$.

Polynomial.roots_list_prod theorem

(L : List R[X]) : (0 : R[X]) ∉ L → L.prod.roots = (L : Multiset R[X]).bind roots

Full source

theorem roots_list_prod (L : List R[X]) :
    (0 : R[X]) ∉ L → L.prod.roots = (L : Multiset R[X]).bind roots :=
  List.recOn L (fun _ => roots_one) fun hd tl ih H => by
    rw [List.mem_cons, not_or] at H
    rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]

Root Multiset Additivity under List Product of Polynomials: $\mathrm{roots}(\prod L) = \sum_{p \in L} \mathrm{roots}(p)$

Informal description

Let $R$ be a commutative ring and let $L$ be a list of polynomials in $R[X]$ such that $0 \notin L$. Then the multiset of roots (with multiplicities) of the product of all polynomials in $L$ is equal to the union (sum) of the multisets of roots of each polynomial in $L$, i.e., \[ \mathrm{roots}\left(\prod_{p \in L} p\right) = \sum_{p \in L} \mathrm{roots}(p). \]

Polynomial.roots_multiset_prod theorem

(m : Multiset R[X]) : (0 : R[X]) ∉ m → m.prod.roots = m.bind roots

Full source

theorem roots_multiset_prod (m : Multiset R[X]) : (0 : R[X]) ∉ m → m.prod.roots = m.bind roots := by
  rcases m with ⟨L⟩
  simpa only [Multiset.prod_coe, quot_mk_to_coe''] using roots_list_prod L

Root Multiset Additivity under Multiset Product of Polynomials: $\mathrm{roots}(\prod m) = \sum_{p \in m} \mathrm{roots}(p)$

Informal description

Let $R$ be a commutative ring and let $m$ be a multiset of polynomials in $R[X]$ such that $0 \notin m$. Then the multiset of roots (with multiplicities) of the product of all polynomials in $m$ is equal to the union (sum) of the multisets of roots of each polynomial in $m$, i.e., \[ \mathrm{roots}\left(\prod_{p \in m} p\right) = \sum_{p \in m} \mathrm{roots}(p). \]

Polynomial.roots_prod theorem

{ι : Type*} (f : ι → R[X]) (s : Finset ι) : s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => roots (f i)

Full source

theorem roots_prod {ι : Type*} (f : ι → R[X]) (s : Finset ι) :
    s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => roots (f i) := by
  rcases s with ⟨m, hm⟩
  simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

Root Multiset Additivity under Finite Product of Polynomials: $\mathrm{roots}(\prod_{i \in s} f(i)) = \sum_{i \in s} \mathrm{roots}(f(i))$

Informal description

Let $R$ be a commutative ring, $\iota$ a type, $f : \iota \to R[X]$ a family of polynomials, and $s$ a finite subset of $\iota$. If the product $\prod_{i \in s} f(i)$ is nonzero, then the multiset of roots (with multiplicities) of this product is equal to the union (sum) of the multisets of roots of each polynomial $f(i)$ for $i \in s$, i.e., \[ \mathrm{roots}\left(\prod_{i \in s} f(i)\right) = \sum_{i \in s} \mathrm{roots}(f(i)). \]

Polynomial.roots_pow theorem

(p : R[X]) (n : ℕ) : (p ^ n).roots = n • p.roots

Full source

@[simp]
theorem roots_pow (p : R[X]) (n : ℕ) : (p ^ n).roots = n • p.roots := by
  induction n with
  | zero => rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
  | succ n ihn =>
    rcases eq_or_ne p 0 with (rfl | hp)
    · rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
    · rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]

Root Multiset Scaling under Polynomial Exponentiation: $\mathrm{roots}(p^n) = n \cdot \mathrm{roots}(p)$

Informal description

For any polynomial $p$ over a commutative ring $R$ and any natural number $n$, the multiset of roots (with multiplicities) of $p^n$ is equal to $n$ times the multiset of roots of $p$, i.e., \[ \mathrm{roots}(p^n) = n \cdot \mathrm{roots}(p). \]

Polynomial.roots_X_pow theorem

(n : ℕ) : (X ^ n : R[X]).roots = n • ({0} : Multiset R)

Full source

theorem roots_X_pow (n : ℕ) : (X ^ n : R[X]).roots = n • ({0} : Multiset R) := by
  rw [roots_pow, roots_X]

Root Multiset of $X^n$: $\mathrm{roots}(X^n) = n \cdot \{0\}$

Informal description

For any natural number $n$, the multiset of roots (with multiplicities) of the polynomial $X^n$ in $R[X]$ is equal to $n$ times the singleton multiset $\{0\}$, i.e., \[ \mathrm{roots}(X^n) = n \cdot \{0\}. \]

Polynomial.roots_C_mul_X_pow theorem

(ha : a ≠ 0) (n : ℕ) : Polynomial.roots (C a * X ^ n) = n • ({0} : Multiset R)

Full source

theorem roots_C_mul_X_pow (ha : a ≠ 0) (n : ℕ) :
    Polynomial.roots (C a * X ^ n) = n • ({0} : Multiset R) := by
  rw [roots_C_mul _ ha, roots_X_pow]

Root Multiset of Monomial $a X^n$: $\mathrm{roots}(a X^n) = n \cdot \{0\}$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a commutative ring $R$ and any natural number $n$, the multiset of roots (with multiplicities) of the polynomial $a X^n$ is equal to $n$ times the singleton multiset $\{0\}$, i.e., \[ \mathrm{roots}(a X^n) = n \cdot \{0\}. \]

Polynomial.roots_monomial theorem

(ha : a ≠ 0) (n : ℕ) : (monomial n a).roots = n • ({0} : Multiset R)

Full source

@[simp]
theorem roots_monomial (ha : a ≠ 0) (n : ℕ) : (monomial n a).roots = n • ({0} : Multiset R) := by
  rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]

Root Multiset of Monomial $a X^n$: $\mathrm{roots}(a X^n) = n \cdot \{0\}$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a commutative ring $R$ and any natural number $n$, the multiset of roots (with multiplicities) of the monomial $a X^n$ is equal to $n$ times the singleton multiset $\{0\}$, i.e., \[ \mathrm{roots}(a X^n) = n \cdot \{0\}. \]

Polynomial.roots_prod_X_sub_C theorem

(s : Finset R) : (s.prod fun a => X - C a).roots = s.val

Full source

theorem roots_prod_X_sub_C (s : Finset R) : (s.prod fun a => X - C a).roots = s.val := by
  apply (roots_prod (fun a => X - C a) s ?_).trans
  · simp_rw [roots_X_sub_C]
    rw [Multiset.bind_singleton, Multiset.map_id']
  · refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

Roots of Product of Linear Factors: $\mathrm{roots}(\prod_{a \in s} (X - a)) = s$

Informal description

For any finite subset $s$ of a commutative ring $R$, the multiset of roots (with multiplicities) of the polynomial $\prod_{a \in s} (X - a)$ is equal to the underlying multiset of $s$.

Polynomial.roots_multiset_prod_X_sub_C theorem

(s : Multiset R) : (s.map fun a => X - C a).prod.roots = s

Full source

@[simp]
theorem roots_multiset_prod_X_sub_C (s : Multiset R) : (s.map fun a => X - C a).prod.roots = s := by
  rw [roots_multiset_prod, Multiset.bind_map]
  · simp_rw [roots_X_sub_C]
    rw [Multiset.bind_singleton, Multiset.map_id']
  · rw [Multiset.mem_map]
    rintro ⟨a, -, h⟩
    exact X_sub_C_ne_zero a h

Roots of Product of Linear Factors: $\mathrm{roots}(\prod_{a \in s} (X - a)) = s$

Informal description

For any multiset $s$ of elements in a commutative ring $R$, the multiset of roots (with multiplicities) of the product of polynomials $\prod_{a \in s} (X - a)$ is equal to $s$ itself. In other words, \[ \mathrm{roots}\left(\prod_{a \in s} (X - a)\right) = s. \]

Polynomial.card_roots_X_pow_sub_C theorem

{n : ℕ} (hn : 0 < n) (a : R) : Multiset.card (roots ((X : R[X]) ^ n - C a)) ≤ n

Full source

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

Upper Bound on Roots of $X^n - a$: $|\text{roots}(X^n - a)| \leq n$

Informal description

For any positive integer $n$ and any element $a$ in a commutative ring $R$, the number of roots (counted with multiplicities) of the polynomial $X^n - a$ is at most $n$. In other words, $|\text{roots}(X^n - a)| \leq n$.

Polynomial.nthRoots definition

(n : ℕ) (a : R) : Multiset R

Full source

/-- `nthRoots n a` noncomputably returns the solutions to `x ^ n = a`. -/
def nthRoots (n : ℕ) (a : R) : Multiset R :=
  roots ((X : R[X]) ^ n - C a)

Solutions to $ x^n = a $ in a commutative ring

Informal description

For a natural number $ n $ and an element $ a $ in a commutative ring $ R $, the multiset `nthRoots n a` consists of all solutions $ x $ in $ R $ to the equation $ x^n = a $. This is defined noncomputably as the roots of the polynomial $ X^n - a $ in $ R[X] $.

Polynomial.mem_nthRoots theorem

{n : ℕ} (hn : 0 < n) {a x : R} : x ∈ nthRoots n a ↔ x ^ n = a

Full source

@[simp]
theorem mem_nthRoots {n : ℕ} (hn : 0 < n) {a x : R} : x ∈ nthRoots n ax ∈ nthRoots n a ↔ x ^ n = a := by
  rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]

Characterization of $n$-th Roots in a Commutative Ring: $x \in \mathrm{nthRoots}(n, a) \iff x^n = a$

Informal description

For a positive integer $n$ and elements $a, x$ in a commutative ring $R$, the element $x$ is in the multiset of $n$-th roots of $a$ if and only if $x^n = a$. That is, \[ x \in \mathrm{nthRoots}(n, a) \iff x^n = a. \]

Polynomial.nthRoots_zero theorem

(r : R) : nthRoots 0 r = 0

Full source

@[simp]
theorem nthRoots_zero (r : R) : nthRoots 0 r = 0 := by
  simp only [empty_eq_zero, pow_zero, nthRoots, ← C_1, ← C_sub, roots_C]

Empty Multiset of Solutions for $x^0 = r$ in a Commutative Ring

Informal description

For any element $r$ in a commutative ring $R$, the multiset of solutions to the equation $x^0 = r$ is empty, i.e., $\text{nthRoots}(0, r) = \emptyset$.

Polynomial.nthRoots_zero_right theorem

{R} [CommRing R] [IsDomain R] (n : ℕ) : nthRoots n (0 : R) = Multiset.replicate n 0

Full source

@[simp]
theorem nthRoots_zero_right {R} [CommRing R] [IsDomain R] (n : ℕ) :
    nthRoots n (0 : R) = Multiset.replicate n 0 := by
  rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]

Solutions to $x^n = 0$ in a domain: $\text{nthRoots}(n, 0) = n \cdot \{0\}$

Informal description

Let $R$ be a commutative ring that is a domain. For any natural number $n$, the multiset of solutions to the equation $x^n = 0$ in $R$ is equal to the multiset containing $n$ copies of $0$, i.e., \[ \text{nthRoots}(n, 0) = \{0, \dots, 0\} \quad \text{($n$ times)}. \]

Polynomial.card_nthRoots theorem

(n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n

Full source

theorem card_nthRoots (n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n := by
  classical exact
  (if hn : n = 0 then
    if h : (X : R[X]) ^ n - C a = 0 then by
      simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]
    else
      WithBot.coe_le_coe.1
        (le_trans (card_roots h)
          (by
            rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
            exact degree_C_le))
  else by
    rw [← Nat.cast_le (α := WithBot ℕ)]
    rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
    exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

Upper Bound on Number of Solutions to $x^n = a$: $|\text{nthRoots}(n, a)| \leq n$

Informal description

For any natural number $n$ and any element $a$ in a commutative ring $R$, the number of distinct solutions (counted with multiplicities) to the equation $x^n = a$ is at most $n$. In other words, the cardinality of the multiset of $n$-th roots of $a$ satisfies $|\text{nthRoots}(n, a)| \leq n$.

Polynomial.nthRoots_two_eq_zero_iff theorem

{r : R} : nthRoots 2 r = 0 ↔ ¬IsSquare r

Full source

@[simp]
theorem nthRoots_two_eq_zero_iff {r : R} : nthRootsnthRoots 2 r = 0 ↔ ¬IsSquare r := by
  simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_not_mem, mem_nthRoots (by norm_num : 0 < 2),
    ← not_exists, eq_comm]

Square Root Existence Criterion: $\mathrm{nthRoots}(2, r) = \emptyset \iff \neg \text{IsSquare}(r)$

Informal description

For any element $r$ in a commutative ring $R$ that is a domain, the multiset of square roots of $r$ is empty if and only if $r$ is not a square in $R$. That is, \[ \mathrm{nthRoots}(2, r) = \emptyset \iff \neg \text{IsSquare}(r). \]

Polynomial.nthRootsFinset definition

(n : ℕ) {R : Type*} (a : R) [CommRing R] [IsDomain R] : Finset R

Full source

/-- The multiset `nthRoots ↑n a` as a Finset. Previously `nthRootsFinset n` was defined to be
`nthRoots n (1 : R)` as a Finset. That situation can be recovered by setting `a` to be `(1 : R)` -/
def nthRootsFinset (n : ℕ) {R : Type*} (a : R) [CommRing R] [IsDomain R] : Finset R :=
  haveI := Classical.decEq R
  Multiset.toFinset (nthRoots n a)

Finite set of distinct solutions to $ x^n = a $ in a commutative domain

Informal description

For a natural number $ n $ and an element $ a $ in a commutative domain $ R $, the finite set `nthRootsFinset n a` consists of all distinct solutions $ x $ in $ R $ to the equation $ x^n = a $. This is obtained by removing duplicates from the multiset of all roots of the polynomial $ X^n - a $ in $ R[X] $.

Polynomial.nthRootsFinset_def theorem

 (n : ℕ) {R : Type*} (a : R) [CommRing R] [IsDomain R] [DecidableEq R] :
  nthRootsFinset n a = Multiset.toFinset (nthRoots n a)

Full source

lemma nthRootsFinset_def (n : ℕ) {R : Type*} (a : R) [CommRing R] [IsDomain R] [DecidableEq R] :
    nthRootsFinset n a = Multiset.toFinset (nthRoots n a) := by
  unfold nthRootsFinset
  convert rfl

Definition of Finite Set of Distinct $n$-th Roots via Multiset Deduplication

Informal description

For any natural number $n$, a commutative domain $R$ with decidable equality, and an element $a \in R$, the finite set of distinct $n$-th roots of $a$ is equal to the finite set obtained by removing duplicates from the multiset of all roots of the polynomial $X^n - a$ in $R[X]$. That is, \[ \text{nthRootsFinset}\, n\, a = \text{toFinset}\, (\text{nthRoots}\, n\, a). \]

Polynomial.mem_nthRootsFinset theorem

{n : ℕ} (h : 0 < n) (a : R) {x : R} : x ∈ nthRootsFinset n a ↔ x ^ (n : ℕ) = a

Full source

@[simp]
theorem mem_nthRootsFinset {n : ℕ} (h : 0 < n) (a : R) {x : R} :
    x ∈ nthRootsFinset n ax ∈ nthRootsFinset n a ↔ x ^ (n : ℕ) = a := by
  classical
  rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

Characterization of Distinct $n$-th Roots in a Commutative Domain: $x \in \mathrm{nthRootsFinset}(n, a) \iff x^n = a$

Informal description

For a positive integer $n$, an element $a$ in a commutative domain $R$, and an element $x \in R$, we have $x$ belongs to the finite set of distinct $n$-th roots of $a$ if and only if $x^n = a$. That is, \[ x \in \mathrm{nthRootsFinset}(n, a) \iff x^n = a. \]

Polynomial.nthRootsFinset_zero theorem

(a : R) : nthRootsFinset 0 a = ∅

Full source

@[simp]
theorem nthRootsFinset_zero (a : R) : nthRootsFinset 0 a = ∅ := by
  classical simp [nthRootsFinset_def]

Empty Set of Solutions for $x^0 = a$ in a Commutative Domain

Informal description

For any element $a$ in a commutative domain $R$, the finite set of distinct solutions to the equation $x^0 = a$ is empty, i.e., $\text{nthRootsFinset}\, 0\, a = \emptyset$.

Polynomial.map_mem_nthRootsFinset theorem

 {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {a : R} {x : R}
  (hx : x ∈ nthRootsFinset n a) (f : F) : f x ∈ nthRootsFinset n (f a)

Full source

theorem map_mem_nthRootsFinset {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S]
    [MonoidHomClass F R S] {a : R} {x : R} (hx : x ∈ nthRootsFinset n a) (f : F) :
    f x ∈ nthRootsFinset n (f a) := by
  by_cases hn : n = 0
  · simp [hn] at hx
  · rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]

Preservation of $n$-th Roots under Monoid Homomorphisms

Informal description

Let $R$ and $S$ be commutative domains, and let $F$ be a type of monoid homomorphisms from $R$ to $S$. For any natural number $n$, any element $a \in R$, and any $x \in R$ such that $x$ is an $n$-th root of $a$ (i.e., $x \in \mathrm{nthRootsFinset}(n, a)$), and for any monoid homomorphism $f \in F$, the image $f(x)$ is an $n$-th root of $f(a)$ in $S$ (i.e., $f(x) \in \mathrm{nthRootsFinset}(n, f(a))$).

Polynomial.map_mem_nthRootsFinset_one theorem

 {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S] [RingHomClass F R S] {x : R} (hx : x ∈ nthRootsFinset n 1)
  (f : F) : f x ∈ nthRootsFinset n 1

Full source

theorem map_mem_nthRootsFinset_one {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S]
    [RingHomClass F R S] {x : R} (hx : x ∈ nthRootsFinset n 1) (f : F) :
    f x ∈ nthRootsFinset n 1 := by
  rw [← (map_one f)]
  exact map_mem_nthRootsFinset hx _

Ring Homomorphisms Preserve Roots of Unity

Informal description

Let $R$ and $S$ be commutative domains, and let $F$ be a type of ring homomorphisms from $R$ to $S$. For any natural number $n$ and any $x \in R$ that is an $n$-th root of unity (i.e., $x \in \text{nthRootsFinset}(n, 1)$), and for any ring homomorphism $f \in F$, the image $f(x)$ is also an $n$-th root of unity in $S$ (i.e., $f(x) \in \text{nthRootsFinset}(n, 1)$).

Polynomial.mul_mem_nthRootsFinset theorem

 {η₁ η₂ : R} {a₁ a₂ : R} (hη₁ : η₁ ∈ nthRootsFinset n a₁) (hη₂ : η₂ ∈ nthRootsFinset n a₂) :
  η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)

Full source

theorem mul_mem_nthRootsFinset
    {η₁ η₂ : R} {a₁ a₂ : R} (hη₁ : η₁ ∈ nthRootsFinset n a₁) (hη₂ : η₂ ∈ nthRootsFinset n a₂) :
    η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂) := by
  cases n with
  | zero =>
    simp only [nthRootsFinset_zero, not_mem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]

Product of $n$-th Roots is $n$-th Root of Product

Informal description

For any elements $\eta_1, \eta_2$ and $a_1, a_2$ in a commutative domain $R$, if $\eta_1$ is an $n$-th root of $a_1$ and $\eta_2$ is an $n$-th root of $a_2$, then their product $\eta_1 \cdot \eta_2$ is an $n$-th root of $a_1 \cdot a_2$. That is, if $\eta_1 \in \text{nthRootsFinset}(n, a_1)$ and $\eta_2 \in \text{nthRootsFinset}(n, a_2)$, then $\eta_1 \cdot \eta_2 \in \text{nthRootsFinset}(n, a_1 \cdot a_2)$.

Polynomial.ne_zero_of_mem_nthRootsFinset theorem

{η : R} {a : R} (ha : a ≠ 0) (hη : η ∈ nthRootsFinset n a) : η ≠ 0

Full source

theorem ne_zero_of_mem_nthRootsFinset {η : R} {a : R} (ha : a ≠ 0) (hη : η ∈ nthRootsFinset n a) :
    η ≠ 0 := by
  nontriviality R
  rintro rfl
  cases n with
  | zero =>
    simp only [nthRootsFinset_zero, not_mem_empty] at hη
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
    exact ha hη.symm

Nonzero $n$-th Roots of Nonzero Elements in a Commutative Domain

Informal description

For any elements $\eta$ and $a$ in a commutative domain $R$, if $a$ is nonzero and $\eta$ is an $n$-th root of $a$ (i.e., $\eta \in \text{nthRootsFinset}(n, a)$), then $\eta$ is also nonzero.

Polynomial.one_mem_nthRootsFinset theorem

(hn : 0 < n) : 1 ∈ nthRootsFinset n (1 : R)

Full source

theorem one_mem_nthRootsFinset (hn : 0 < n) : 1 ∈ nthRootsFinset n (1 : R) := by
  rw [mem_nthRootsFinset hn, one_pow]

$1$ is an $n$-th root of unity for $n > 0$

Informal description

For any positive integer $n$, the multiplicative identity $1$ is an $n$-th root of unity in a commutative domain $R$, i.e., $1 \in \text{nthRootsFinset}(n, 1)$.

Polynomial.zero_of_eval_zero theorem

[Infinite R] (p : R[X]) (h : ∀ x, p.eval x = 0) : p = 0

Full source

theorem zero_of_eval_zero [Infinite R] (p : R[X]) (h : ∀ x, p.eval x = 0) : p = 0 := by
  classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

Vanishing Polynomial over Infinite Ring is Zero

Informal description

Let $R$ be an infinite commutative ring and $p \in R[X]$ a polynomial. If $p$ evaluates to zero at every element of $R$, then $p$ is the zero polynomial.

Polynomial.funext theorem

[Infinite R] {p q : R[X]} (ext : ∀ r : R, p.eval r = q.eval r) : p = q

Full source

theorem funext [Infinite R] {p q : R[X]} (ext : ∀ r : R, p.eval r = q.eval r) : p = q := by
  rw [← sub_eq_zero]
  apply zero_of_eval_zero
  intro x
  rw [eval_sub, sub_eq_zero, ext]

Polynomial Functional Extensionality over Infinite Rings

Informal description

Let $R$ be an infinite commutative ring and $p, q \in R[X]$ be polynomials. If $p$ and $q$ evaluate to the same value at every element of $R$, then $p = q$.

Polynomial.aroots abbrev

(p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Multiset S

Full source

/-- Given a polynomial `p` with coefficients in a ring `T` and a `T`-algebra `S`, `aroots p S` is
the multiset of roots of `p` regarded as a polynomial over `S`. -/
noncomputable abbrev aroots (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Multiset S :=
  (p.map (algebraMap T S)).roots

Multiset of roots of a polynomial in an algebra extension

Informal description

Given a polynomial $p$ with coefficients in a commutative ring $T$ and a $T$-algebra $S$ that is a commutative domain, the multiset $\text{aroots}(p, S)$ consists of all roots of $p$ when regarded as a polynomial over $S$, with each root appearing according to its multiplicity.

Polynomial.aroots_def theorem

(p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : p.aroots S = (p.map (algebraMap T S)).roots

Full source

theorem aroots_def (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] :
    p.aroots S = (p.map (algebraMap T S)).roots :=
  rfl

Equality of Root Multisets under Algebra Extension

Informal description

For a polynomial $p$ with coefficients in a commutative ring $T$ and a $T$-algebra $S$ that is a commutative domain, the multiset of roots of $p$ in $S$ (with multiplicities) is equal to the multiset of roots of the polynomial obtained by mapping the coefficients of $p$ into $S$ via the algebra map. That is, $\text{aroots}(p, S) = \text{roots}(p \circ \text{algebraMap}(T, S))$.

Polynomial.mem_aroots' theorem

 [CommRing S] [IsDomain S] [Algebra T S] {p : T[X]} {a : S} :
  a ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0

Full source

theorem mem_aroots' [CommRing S] [IsDomain S] [Algebra T S] {p : T[X]} {a : S} :
    a ∈ p.aroots Sa ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0 := by
  rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]

Characterization of Root Membership in Algebra Extension: $a \in \text{aroots}(p, S) \iff (p \circ \text{algebraMap} \neq 0) \land (p(a) = 0)$

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$ and any element $a \in S$, the following are equivalent: 1. $a$ is a root of $p$ in $S$ (i.e., $a$ appears in the multiset $\text{aroots}(p, S)$) 2. The polynomial $p$ mapped to $S[X]$ via the algebra map is nonzero, and the evaluation of $p$ at $a$ is zero. In other words: \[ a \in \text{aroots}(p, S) \iff (p \circ \text{algebraMap}(T, S) \neq 0) \land (\text{aeval}(a, p) = 0) \]

Polynomial.mem_aroots theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : T[X]} {a : S} :
  a ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0

Full source

theorem mem_aroots [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {p : T[X]} {a : S} : a ∈ p.aroots Sa ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0 := by
  rw [mem_aroots', Polynomial.map_ne_zero_iff]
  exact FaithfulSMul.algebraMap_injective T S

Characterization of Root Membership in Polynomial Algebra with No Zero Divisors

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero polynomial $p \in T[X]$ and any element $a \in S$, the element $a$ is a root of $p$ in $S$ (i.e., $a$ appears in the multiset $\text{aroots}(p, S)$) if and only if the evaluation of $p$ at $a$ is zero, i.e., $\text{aeval}(a, p) = 0$. In other words: \[ a \in \text{aroots}(p, S) \iff (p \neq 0) \land (p(a) = 0) \]

Polynomial.aroots_mul theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p q : T[X]} (hpq : p * q ≠ 0) :
  (p * q).aroots S = p.aroots S + q.aroots S

Full source

theorem aroots_mul [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {p q : T[X]} (hpq : p * q ≠ 0) :
    (p * q).aroots S = p.aroots S + q.aroots S := by
  suffices mapmap (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
    rw [aroots_def, Polynomial.map_mul, roots_mul this]
  rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff
    (FaithfulSMul.algebraMap_injective T S)]

Additivity of Root Multisets under Polynomial Multiplication in Algebra Extensions: $\mathrm{aroots}(p \cdot q, S) = \mathrm{aroots}(p, S) + \mathrm{aroots}(q, S)$

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero polynomials $p, q \in T[X]$ such that their product $p \cdot q$ is also nonzero, the multiset of roots of $p \cdot q$ in $S$ (with multiplicities) is equal to the sum of the multisets of roots of $p$ and $q$ in $S$. That is, \[ \mathrm{aroots}(p \cdot q, S) = \mathrm{aroots}(p, S) + \mathrm{aroots}(q, S). \]

Polynomial.aroots_X_sub_C theorem

[CommRing S] [IsDomain S] [Algebra T S] (r : T) : aroots (X - C r) S = {algebraMap T S r}

Full source

@[simp]
theorem aroots_X_sub_C [CommRing S] [IsDomain S] [Algebra T S]
    (r : T) : aroots (X - C r) S = {algebraMap T S r} := by
  rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]

Roots of Linear Polynomial in Algebra Extension: $\text{aroots}(X - r, S) = \{\text{algebraMap}(r)\}$

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any element $r \in T$, the multiset of roots of the polynomial $X - r$ in $S$ is the singleton multiset containing the image of $r$ under the algebra map from $T$ to $S$, i.e., \[ \text{aroots}(X - r, S) = \{\text{algebraMap}(T, S)(r)\}. \]

Polynomial.aroots_X theorem

[CommRing S] [IsDomain S] [Algebra T S] : aroots (X : T[X]) S = {0}

Full source

@[simp]
theorem aroots_X [CommRing S] [IsDomain S] [Algebra T S] :
    aroots (X : T[X]) S = {0} := by
  rw [aroots_def, map_X, roots_X]

Roots of the Polynomial $X$ in Algebra Extension: $\text{aroots}(X, S) = \{0\}$

Informal description

Let $S$ be a commutative domain that is an algebra over a commutative ring $T$. The multiset of roots of the polynomial $X$ in $S$ is the singleton multiset $\{0\}$.

Polynomial.aroots_C theorem

[CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).aroots S = 0

Full source

@[simp]
theorem aroots_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).aroots S = 0 := by
  rw [aroots_def, map_C, roots_C]

Constant Polynomial Has No Roots in Algebra Extension

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, and for any element $a \in T$, the multiset of roots of the constant polynomial $C(a)$ in $S$ is empty, i.e., $\text{aroots}(C(a), S) = \emptyset$.

Polynomial.aroots_zero theorem

(S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).aroots S = 0

Full source

@[simp]
theorem aroots_zero (S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).aroots S = 0 := by
  rw [← C_0, aroots_C]

Zero Polynomial Has No Roots in Algebra Extension

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, the multiset of roots of the zero polynomial in $S$ is empty, i.e., $\text{aroots}(0, S) = \emptyset$.

Polynomial.aroots_one theorem

[CommRing S] [IsDomain S] [Algebra T S] : (1 : T[X]).aroots S = 0

Full source

@[simp]
theorem aroots_one [CommRing S] [IsDomain S] [Algebra T S] :
    (1 : T[X]).aroots S = 0 :=
  aroots_C 1

Constant One Polynomial Has No Roots in Algebra Extension

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, the multiset of roots of the constant polynomial $1$ in $S$ is empty, i.e., $\text{aroots}(1, S) = \emptyset$.

Polynomial.aroots_neg theorem

[CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) : (-p).aroots S = p.aroots S

Full source

@[simp]
theorem aroots_neg [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) :
    (-p).aroots S = p.aroots S := by
  rw [aroots, Polynomial.map_neg, roots_neg]

Root Multiset Invariance under Negation in Algebra Extension: $\text{aroots}(-p, S) = \text{aroots}(p, S)$

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$, the multiset of roots of $-p$ in $S$ is equal to the multiset of roots of $p$ in $S$, i.e., \[ \text{aroots}(-p, S) = \text{aroots}(p, S). \]

Polynomial.aroots_C_mul theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
  (C a * p).aroots S = p.aroots S

Full source

@[simp]
theorem aroots_C_mul [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
    (C a * p).aroots S = p.aroots S := by
  rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]
  rwa [map_ne_zero_iff]
  exact FaithfulSMul.algebraMap_injective T S

Root Multiset Invariance under Nonzero Scalar Multiplication in Algebra Extension

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero element $a \in T$ and any polynomial $p \in T[X]$, the multiset of roots of the polynomial $C(a) \cdot p$ in $S$ is equal to the multiset of roots of $p$ in $S$, i.e., \[ \text{aroots}(C(a) \cdot p, S) = \text{aroots}(p, S). \]

Polynomial.aroots_smul_nonzero theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
  (a • p).aroots S = p.aroots S

Full source

@[simp]
theorem aroots_smul_nonzero [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
    (a • p).aroots S = p.aroots S := by
  rw [smul_eq_C_mul, aroots_C_mul _ ha]

Root Multiset Invariance under Nonzero Scalar Multiplication in Algebra Extension

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero element $a \in T$ and any polynomial $p \in T[X]$, the multiset of roots of the scalar multiple $a \cdot p$ in $S$ is equal to the multiset of roots of $p$ in $S$, i.e., \[ \text{aroots}(a \cdot p, S) = \text{aroots}(p, S). \]

Polynomial.aroots_pow theorem

[CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) (n : ℕ) : (p ^ n).aroots S = n • p.aroots S

Full source

@[simp]
theorem aroots_pow [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) (n : ℕ) :
    (p ^ n).aroots S = n • p.aroots S := by
  rw [aroots_def, Polynomial.map_pow, roots_pow]

Root Multiplicity Scaling under Polynomial Exponentiation: $\text{aroots}(p^n, S) = n \cdot \text{aroots}(p, S)$

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$ and natural number $n$, the multiset of roots of $p^n$ in $S$ (counted with multiplicities) is equal to $n$ times the multiset of roots of $p$ in $S$. That is, \[ \text{aroots}(p^n, S) = n \cdot \text{aroots}(p, S). \]

Polynomial.aroots_X_pow theorem

[CommRing S] [IsDomain S] [Algebra T S] (n : ℕ) : (X ^ n : T[X]).aroots S = n • ({0} : Multiset S)

Full source

theorem aroots_X_pow [CommRing S] [IsDomain S] [Algebra T S] (n : ℕ) :
    (X ^ n : T[X]).aroots S = n • ({0} : Multiset S) := by
  rw [aroots_pow, aroots_X]

Root Multiset of $X^n$ in Algebra Extension: $\text{aroots}(X^n, S) = n \cdot \{0\}$

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any natural number $n$, the multiset of roots of the polynomial $X^n$ in $S$ (counted with multiplicities) is equal to $n$ times the singleton multiset $\{0\}$. That is, \[ \text{aroots}(X^n, S) = n \cdot \{0\}. \]

Polynomial.aroots_C_mul_X_pow theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
  (C a * X ^ n : T[X]).aroots S = n • ({0} : Multiset S)

Full source

theorem aroots_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
    (C a * X ^ n : T[X]).aroots S = n • ({0} : Multiset S) := by
  rw [aroots_C_mul _ ha, aroots_X_pow]

Root multiset of monomial $aX^n$ in algebra extension: $\text{aroots}(aX^n, S) = n \cdot \{0\}$

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero element $a \in T$ and any natural number $n$, the multiset of roots of the polynomial $aX^n$ in $S$ is equal to $n$ times the singleton multiset $\{0\}$. That is, \[ \text{aroots}(aX^n, S) = n \cdot \{0\}. \]

Polynomial.aroots_monomial theorem

 [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
  (monomial n a).aroots S = n • ({0} : Multiset S)

Full source

@[simp]
theorem aroots_monomial [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
    (monomial n a).aroots S = n • ({0} : Multiset S) := by
  rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]

Root multiset of monomial $aX^n$ in algebra extension: $\text{aroots}(aX^n, S) = n \cdot \{0\}$

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero element $a \in T$ and any natural number $n$, the multiset of roots of the monomial $aX^n$ in $S$ is equal to $n$ times the singleton multiset $\{0\}$. That is, \[ \text{aroots}(aX^n, S) = n \cdot \{0\}. \]

Polynomial.aroots_map theorem

 (p : T[X]) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R] [IsScalarTower T S R] :
  (p.map (algebraMap T S)).aroots R = p.aroots R

Full source

@[simp]
theorem aroots_map (p : T[X]) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R]
    [IsScalarTower T S R] :
    (p.map (algebraMap T S)).aroots R = p.aroots R := by
  rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

Root Multiset Preservation under Coefficient Mapping in Scalar Tower

Informal description

Let $T$, $S$, and $R$ be commutative rings with $S$ and $R$ being domains, and let there be algebra structures $T \to S \to R$ forming a scalar tower. For any polynomial $p \in T[X]$, the multiset of roots of $p$ in $R$ is equal to the multiset of roots of the polynomial obtained by first mapping $p$'s coefficients from $T$ to $S$ and then considering it in $R$. That is, $\text{aroots}(p \circ \text{algebraMap}(T, S), R) = \text{aroots}(p, R)$.

Polynomial.rootSet definition

(p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Set S

Full source

/-- The set of distinct roots of `p` in `S`.

If you have a non-separable polynomial, use `Polynomial.aroots` for the multiset
where multiple roots have the appropriate multiplicity. -/
def rootSet (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Set S :=
  haveI := Classical.decEq S
  (p.aroots S).toFinset

Set of distinct roots of a polynomial in an algebra extension

Informal description

Given a polynomial $p$ with coefficients in a commutative ring $T$ and a $T$-algebra $S$ that is a commutative domain, the set $\text{rootSet}(p, S)$ consists of all distinct roots of $p$ when regarded as a polynomial over $S$. This is obtained by converting the multiset of roots (with multiplicities) to a set via deduplication.

Polynomial.rootSet_def theorem

(p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] [DecidableEq S] : p.rootSet S = (p.aroots S).toFinset

Full source

theorem rootSet_def (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] [DecidableEq S] :
    p.rootSet S = (p.aroots S).toFinset := by
  rw [rootSet]
  convert rfl

Characterization of Root Set as Deduplicated Multiset of Roots

Informal description

For a polynomial $p$ with coefficients in a commutative ring $T$, and a $T$-algebra $S$ that is a commutative domain with decidable equality, the set of distinct roots $\text{rootSet}(p, S)$ is equal to the finite set obtained by removing duplicates from the multiset of roots $\text{aroots}(p, S)$.

Polynomial.rootSet_C theorem

[CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).rootSet S = ∅

Full source

@[simp]
theorem rootSet_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).rootSet S = ∅ := by
  classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

Empty Root Set for Constant Polynomials

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, and for any element $a \in T$, the set of distinct roots of the constant polynomial $C(a)$ in $S$ is empty, i.e., $\text{rootSet}(C(a), S) = \emptyset$.

Polynomial.rootSet_zero theorem

(S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).rootSet S = ∅

Full source

@[simp]
theorem rootSet_zero (S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).rootSet S = ∅ := by
  rw [← C_0, rootSet_C]

Empty Root Set for the Zero Polynomial

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, the set of distinct roots of the zero polynomial in $S$ is empty, i.e., $\text{rootSet}(0, S) = \emptyset$.

Polynomial.rootSet_one theorem

(S) [CommRing S] [IsDomain S] [Algebra T S] : (1 : T[X]).rootSet S = ∅

Full source

@[simp]
theorem rootSet_one (S) [CommRing S] [IsDomain S] [Algebra T S] : (1 : T[X]).rootSet S = ∅ := by
  rw [← C_1, rootSet_C]

Empty Root Set for the Unit Polynomial

Informal description

For any commutative domain $S$ that is an algebra over a commutative ring $T$, the set of distinct roots of the constant polynomial $1$ in $S$ is empty, i.e., $\text{rootSet}(1, S) = \emptyset$.

Polynomial.rootSet_neg theorem

(p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : (-p).rootSet S = p.rootSet S

Full source

@[simp]
theorem rootSet_neg (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] :
    (-p).rootSet S = p.rootSet S := by
  rw [rootSet, aroots_neg, rootSet]

Root Set Invariance under Negation: $\text{rootSet}(-p, S) = \text{rootSet}(p, S)$

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$, the set of distinct roots of $-p$ in $S$ is equal to the set of distinct roots of $p$ in $S$, i.e., \[ \text{rootSet}(-p, S) = \text{rootSet}(p, S). \]

Polynomial.rootSetFintype instance

(p : T[X]) (S : Type*) [CommRing S] [IsDomain S] [Algebra T S] : Fintype (p.rootSet S)

Full source

instance rootSetFintype (p : T[X]) (S : Type*) [CommRing S] [IsDomain S] [Algebra T S] :
    Fintype (p.rootSet S) :=
  FinsetCoe.fintype _

Finiteness of the Root Set of a Polynomial in a Domain

Informal description

For any polynomial $p$ with coefficients in a commutative ring $T$ and any commutative domain $S$ that is a $T$-algebra, the set of distinct roots of $p$ in $S$ is finite.

Polynomial.rootSet_finite theorem

(p : T[X]) (S : Type*) [CommRing S] [IsDomain S] [Algebra T S] : (p.rootSet S).Finite

Full source

theorem rootSet_finite (p : T[X]) (S : Type*) [CommRing S] [IsDomain S] [Algebra T S] :
    (p.rootSet S).Finite :=
  Set.toFinite _

Finiteness of the Root Set of a Polynomial in a Domain

Informal description

For any polynomial $p$ with coefficients in a commutative ring $T$ and any commutative domain $S$ that is a $T$-algebra, the set of distinct roots of $p$ in $S$ is finite.

Polynomial.bUnion_roots_finite theorem

 {R S : Type*} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ) {U : Set R} (h : U.Finite) :
  (⋃ (f : R[X]) (_ : f.natDegree ≤ d ∧ ∀ i, f.coeff i ∈ U), ((f.map m).roots.toFinset.toSet : Set S)).Finite

Full source

/-- The set of roots of all polynomials of bounded degree and having coefficients in a finite set
is finite. -/
theorem bUnion_roots_finite {R S : Type*} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S]
    (m : R →+* S) (d : ℕ) {U : Set R} (h : U.Finite) :
    (⋃ (f : R[X]) (_ : f.natDegree ≤ d ∧ ∀ i, f.coeff i ∈ U),
        ((f.map m).roots.toFinset.toSet : Set S)).Finite :=
  Set.Finite.biUnion
    (by
      -- We prove that the set of polynomials under consideration is finite because its
      -- image by the injective map `π` is finite
      let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i
      refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
      · exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i
      · refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
        exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩)
    fun _ _ => Finset.finite_toSet _

Finiteness of Roots of Bounded-Degree Polynomials with Coefficients in a Finite Set

Informal description

Let $R$ be a semiring and $S$ be a commutative domain with a ring homomorphism $m \colon R \to S$. For any natural number $d$ and any finite subset $U \subseteq R$, the union of the root sets (as sets of distinct roots) of all polynomials $f \in R[X]$ with degree at most $d$ and coefficients in $U$ is finite. In other words, the set \[ \bigcup_{\substack{f \in R[X] \\ \deg(f) \leq d \\ \forall i, f_i \in U}} \{ \text{distinct roots of } f \text{ in } S \} \] is finite.

Polynomial.mem_rootSet' theorem

 {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] {a : S} :
  a ∈ p.rootSet S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0

Full source

theorem mem_rootSet' {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] {a : S} :
    a ∈ p.rootSet Sa ∈ p.rootSet S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0 := by
  classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Characterization of Root Set Membership in Algebra Extension

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$ and any element $a \in S$, the following are equivalent: 1. $a$ belongs to the root set of $p$ in $S$, i.e., $a \in \text{rootSet}(p, S)$. 2. The polynomial $p$ mapped to $S[X]$ via the algebra map is nonzero, and the evaluation of $p$ at $a$ is zero. In other words: \[ a \in \text{rootSet}(p, S) \iff (p \circ \text{algebraMap}(T, S) \neq 0) \land (p(a) = 0) \]

Polynomial.mem_rootSet theorem

 {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : S} :
  a ∈ p.rootSet S ↔ p ≠ 0 ∧ aeval a p = 0

Full source

theorem mem_rootSet {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : S} : a ∈ p.rootSet Sa ∈ p.rootSet S ↔ p ≠ 0 ∧ aeval a p = 0 := by
  rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

Characterization of Root Set Membership in Algebra Extension with No Zero Divisors

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero polynomial $p \in T[X]$ and any element $a \in S$, the following are equivalent: 1. $a$ belongs to the root set of $p$ in $S$, i.e., $a \in \text{rootSet}(p, S)$. 2. The evaluation of $p$ at $a$ is zero, i.e., $p(a) = 0$. In other words: \[ a \in \text{rootSet}(p, S) \iff (p \neq 0) \land (p(a) = 0) \]

Polynomial.mem_rootSet_of_ne theorem

 {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] (hp : p ≠ 0) {a : S} :
  a ∈ p.rootSet S ↔ aeval a p = 0

Full source

theorem mem_rootSet_of_ne {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] (hp : p ≠ 0) {a : S} : a ∈ p.rootSet Sa ∈ p.rootSet S ↔ aeval a p = 0 :=
  mem_rootSet.trans <| and_iff_right hp

Characterization of root set membership for nonzero polynomials

Informal description

Let $T$ be a commutative ring and $S$ a commutative domain that is a $T$-algebra with no zero scalar divisors. For any nonzero polynomial $p \in T[X]$ and any element $a \in S$, the following are equivalent: 1. $a$ is in the root set of $p$ in $S$, i.e., $a \in \text{rootSet}(p, S)$. 2. The evaluation of $p$ at $a$ is zero, i.e., $p(a) = 0$. In other words: \[ a \in \text{rootSet}(p, S) \iff p(a) = 0 \]

Polynomial.rootSet_maps_to' theorem

 {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S']
  (hp : p.map (algebraMap T S') = 0 → p.map (algebraMap T S) = 0) (f : S →ₐ[T] S') :
  (p.rootSet S).MapsTo f (p.rootSet S')

Full source

theorem rootSet_maps_to' {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S']
    [IsDomain S'] [Algebra T S'] (hp : p.map (algebraMap T S') = 0 → p.map (algebraMap T S) = 0)
    (f : S →ₐ[T] S') : (p.rootSet S).MapsTo f (p.rootSet S') := fun x hx => by
  rw [mem_rootSet'] at hx ⊢
  rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
  exact ⟨mt hp hx.1, rfl⟩

Mapping of Roots Under Algebra Homomorphism: $f(\text{rootSet}(p, S)) \subseteq \text{rootSet}(p, S')$

Informal description

Let $T$ be a commutative ring, and let $S$ and $S'$ be commutative domains that are $T$-algebras. Given a polynomial $p \in T[X]$ and a $T$-algebra homomorphism $f \colon S \to S'$, if the condition $p \circ \text{algebraMap}(T, S') = 0$ implies $p \circ \text{algebraMap}(T, S) = 0$, then $f$ maps every element of the root set of $p$ in $S$ to an element of the root set of $p$ in $S'$. That is, for every $a \in \text{rootSet}(p, S)$, we have $f(a) \in \text{rootSet}(p, S')$.

Polynomial.ne_zero_of_mem_rootSet theorem

{p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (h : a ∈ p.rootSet S) : p ≠ 0

Full source

theorem ne_zero_of_mem_rootSet {p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S}
    (h : a ∈ p.rootSet S) : p ≠ 0 := fun hf => by rwa [hf, rootSet_zero] at h

Nonzero Polynomial Condition for Membership in Root Set

Informal description

For any polynomial $p$ with coefficients in a commutative ring $T$, and any commutative domain $S$ that is a $T$-algebra, if an element $a \in S$ is in the root set of $p$ (i.e., $a \in \text{rootSet}(p, S)$), then $p$ is not the zero polynomial.

Polynomial.aeval_eq_zero_of_mem_rootSet theorem

{p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (hx : a ∈ p.rootSet S) : aeval a p = 0

Full source

theorem aeval_eq_zero_of_mem_rootSet {p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S}
    (hx : a ∈ p.rootSet S) : aeval a p = 0 :=
  (mem_rootSet'.1 hx).2

Evaluation Vanishes on Root Set Elements

Informal description

Let $T$ be a commutative ring and $S$ be a commutative domain that is a $T$-algebra. For any polynomial $p \in T[X]$ and any element $a \in S$, if $a$ belongs to the root set of $p$ in $S$ (i.e., $a \in \text{rootSet}(p, S)$), then the evaluation of $p$ at $a$ is zero, i.e., $p(a) = 0$.

Polynomial.rootSet_mapsTo theorem

 {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S']
  [NoZeroSMulDivisors T S'] (f : S →ₐ[T] S') : (p.rootSet S).MapsTo f (p.rootSet S')

Full source

theorem rootSet_mapsTo {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S']
    [IsDomain S'] [Algebra T S'] [NoZeroSMulDivisors T S'] (f : S →ₐ[T] S') :
    (p.rootSet S).MapsTo f (p.rootSet S') := by
  refine rootSet_maps_to' (fun h₀ => ?_) f
  obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])
  exact Polynomial.map_zero _

Mapping of Roots Under Algebra Homomorphism: $f(\text{rootSet}(p, S)) \subseteq \text{rootSet}(p, S')$

Informal description

Let $T$ be a commutative ring, and let $S$ and $S'$ be commutative domains that are $T$-algebras, with $S'$ having no zero scalar divisors over $T$. Given a polynomial $p \in T[X]$ and a $T$-algebra homomorphism $f \colon S \to S'$, the image of the root set $\text{rootSet}(p, S)$ under $f$ is contained in the root set $\text{rootSet}(p, S')$. That is, for every $a \in \text{rootSet}(p, S)$, we have $f(a) \in \text{rootSet}(p, S')$.

Polynomial.mem_rootSet_of_injective theorem

 [CommRing S] {p : S[X]} [Algebra S R] (h : Function.Injective (algebraMap S R)) {x : R} (hp : p ≠ 0) :
  x ∈ p.rootSet R ↔ aeval x p = 0

Full source

theorem mem_rootSet_of_injective [CommRing S] {p : S[X]} [Algebra S R]
    (h : Function.Injective (algebraMap S R)) {x : R} (hp : p ≠ 0) :
    x ∈ p.rootSet Rx ∈ p.rootSet R ↔ aeval x p = 0 := by
  classical
  exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

Characterization of roots in algebra extension via injective algebra map

Informal description

Let $S$ and $R$ be commutative rings with $S$ a domain, and let $p \neq 0$ be a polynomial over $S$. Suppose the algebra map $\text{algebraMap}\, S\, R$ is injective. Then for any $x \in R$, we have $x \in \text{rootSet}(p, R)$ if and only if the evaluation of $p$ at $x$ via the algebra map is zero, i.e., $\text{aeval}\, x\, p = 0$.

Polynomial.exists_eval_ne_zero_of_natDegree_lt_card theorem

(f : R[X]) (hf : f ≠ 0) (hfR : f.natDegree < #R) : ∃ r, f.eval r ≠ 0

Full source

lemma exists_eval_ne_zero_of_natDegree_lt_card (f : R[X]) (hf : f ≠ 0) (hfR : f.natDegree < #R) :
    ∃ r, f.eval r ≠ 0 := by
  contrapose! hf
  exact eq_zero_of_forall_eval_zero_of_natDegree_lt_card f hf hfR

Existence of Non-Root for Polynomial with Degree Less Than Ring Cardinality

Informal description

Let $R$ be a commutative ring that is a domain, and let $f \in R[X]$ be a nonzero polynomial. If the natural degree of $f$ is strictly less than the cardinality of $R$, then there exists an element $r \in R$ such that the evaluation of $f$ at $r$ is nonzero, i.e., $f(r) \neq 0$.

Polynomial.monic_multisetProd_X_sub_C theorem

(s : Multiset R) : Monic (s.map fun a => X - C a).prod

Full source

theorem monic_multisetProd_X_sub_C (s : Multiset R) : Monic (s.map fun a => X - C a).prod :=
  monic_multiset_prod_of_monic _ _ fun a _ => monic_X_sub_C a

Monic Property of Product $\prod_{a \in s} (X - a)$

Informal description

For any multiset $s$ over a commutative ring $R$, the product $\prod_{a \in s} (X - a)$ is a monic polynomial in $R[X]$.

Polynomial.monic_prod_X_sub_C theorem

{α : Type*} (b : α → R) (s : Finset α) : Monic (∏ a ∈ s, (X - C (b a)))

Full source

theorem monic_prod_X_sub_C {α : Type*} (b : α → R) (s : Finset α) :
    Monic (∏ a ∈ s, (X - C (b a))) :=
  monic_prod_of_monic _ _ fun a _ => monic_X_sub_C (b a)

Product of Linear Factors $(X - b(a))$ is Monic

Informal description

Let $R$ be a commutative ring and let $s$ be a finite set indexed by a type $\alpha$. Given a function $b : \alpha \to R$, the product $\prod_{a \in s} (X - b(a))$ is a monic polynomial in $R[X]$.

Polynomial.monic_finprod_X_sub_C theorem

{α : Type*} (b : α → R) : Monic (∏ᶠ k, (X - C (b k)))

Full source

theorem monic_finprod_X_sub_C {α : Type*} (b : α → R) : Monic (∏ᶠ k, (X - C (b k))) :=
  monic_finprod_of_monic _ _ fun a _ => monic_X_sub_C (b a)

Monic Property of Finitary Product of Linear Factors $(X - b(k))$

Informal description

For any commutative ring $R$ and any function $b : \alpha \to R$, the finitary product $\prodᶠ_{k} (X - b(k))$ is a monic polynomial in $R[X]$, meaning its leading coefficient is $1$.

Polynomial.prod_multiset_root_eq_finset_root theorem

[DecidableEq R] : (p.roots.map fun a => X - C a).prod = p.roots.toFinset.prod fun a => (X - C a) ^ rootMultiplicity a p

Full source

theorem prod_multiset_root_eq_finset_root [DecidableEq R] :
    (p.roots.map fun a => X - C a).prod =
      p.roots.toFinset.prod fun a => (X - C a) ^ rootMultiplicity a p := by
  simp only [count_roots, Finset.prod_multiset_map_count]

Product of Linear Factors over Roots with Multiplicities

Informal description

Let $R$ be a commutative ring with decidable equality and $p \in R[X]$ a polynomial. The product of the linear factors $(X - a)$ over all roots $a$ in the multiset of roots of $p$ (counting multiplicities) is equal to the product of $(X - a)^{\text{rootMultiplicity}(a, p)}$ over the distinct roots $a$ in the finite set of roots of $p$. That is, \[ \prod_{a \in \text{roots}(p)} (X - a) = \prod_{a \in \text{roots}(p).\text{toFinset}} (X - a)^{\text{rootMultiplicity}(a, p)}. \]

Polynomial.prod_multiset_X_sub_C_dvd theorem

(p : R[X]) : (p.roots.map fun a => X - C a).prod ∣ p

Full source

/-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
theorem prod_multiset_X_sub_C_dvd (p : R[X]) : (p.roots.map fun a => X - C a).prod ∣ p := by
  classical
  rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)

Divisibility by Product of Linear Factors from Roots: $\prod_{a \in \text{roots}(p)} (X - a) \mid p$

Informal description

For any polynomial $p$ over a commutative ring $R$, the product $\prod_{a \in \text{roots}(p)} (X - a)$ divides $p$, where $\text{roots}(p)$ denotes the multiset of roots of $p$ (with multiplicities).

Multiset.prod_X_sub_C_dvd_iff_le_roots theorem

{p : R[X]} (hp : p ≠ 0) (s : Multiset R) : (s.map fun a => X - C a).prod ∣ p ↔ s ≤ p.roots

Full source

/-- A Galois connection. -/
theorem _root_.Multiset.prod_X_sub_C_dvd_iff_le_roots {p : R[X]} (hp : p ≠ 0) (s : Multiset R) :
    (s.map fun a => X - C a).prod ∣ p(s.map fun a => X - C a).prod ∣ p ↔ s ≤ p.roots := by
  classical exact
  ⟨fun h =>
    Multiset.le_iff_count.2 fun r => by
      rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
      exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
    fun h =>
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

Divisibility by Product of Linear Factors from Sub-multiset of Roots

Informal description

Let $R$ be a commutative ring and $p \in R[X]$ a nonzero polynomial. For any multiset $s$ of elements in $R$, the product $\prod_{a \in s} (X - a)$ divides $p$ if and only if $s$ is a sub-multiset of the roots of $p$ (counting multiplicities). That is, \[ \prod_{a \in s} (X - a) \mid p \quad \leftrightarrow \quad s \leq \text{roots}(p). \]

Polynomial.exists_prod_multiset_X_sub_C_mul theorem

 (p : R[X]) :
  ∃ q, (p.roots.map fun a => X - C a).prod * q = p ∧ Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0

Full source

theorem exists_prod_multiset_X_sub_C_mul (p : R[X]) :
    ∃ q,
      (p.roots.map fun a => X - C a).prod * q = p ∧
        Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0 := by
  obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd
  use q, he.symm
  obtain rfl | hq := eq_or_ne q 0
  · rw [mul_zero] at he
    subst he
    simp
  constructor
  · conv_rhs => rw [he]
    rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]
  · replace he := congr_arg roots he.symm
    rw [roots_mul, roots_multiset_prod_X_sub_C] at he
    exacts [add_eq_left.1 he, mul_ne_zero (monic_multisetProd_X_sub_C p.roots).ne_zero hq]

Factorization of Polynomial into Linear Factors and Root-Free Remainder

Informal description

For any polynomial $p$ over a commutative ring $R$, there exists a polynomial $q$ such that: 1. $p$ factors as $(\prod_{a \in \text{roots}(p)} (X - a)) \cdot q$, 2. The sum of the number of roots (counting multiplicities) and the degree of $q$ equals the degree of $p$, 3. The polynomial $q$ has no roots (i.e., $\text{roots}(q) = \emptyset$).

Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C theorem

(hroots : Multiset.card p.roots = p.natDegree) : C p.leadingCoeff * (p.roots.map fun a => X - C a).prod = p

Full source

/-- A polynomial `p` that has as many roots as its degree
can be written `p = p.leadingCoeff * ∏(X - a)`, for `a` in `p.roots`. -/
theorem C_leadingCoeff_mul_prod_multiset_X_sub_C (hroots : Multiset.card p.roots = p.natDegree) :
    C p.leadingCoeff * (p.roots.map fun a => X - C a).prod = p :=
  (eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le (monic_multisetProd_X_sub_C p.roots)
      p.prod_multiset_X_sub_C_dvd
      ((natDegree_multiset_prod_X_sub_C_eq_card _).trans hroots).ge).symm

Factorization of Polynomial with Full Root Count: $p = C(p_{\text{leadingCoeff}}) \cdot \prod (X - a)$

Informal description

Let $p$ be a polynomial over a commutative ring $R$ such that the number of roots (counting multiplicities) equals its degree. Then $p$ can be expressed as the product of its leading coefficient and the product of linear terms $(X - a)$ for each root $a$ in its multiset of roots, i.e., \[ p = C(p_{\text{leadingCoeff}}) \cdot \prod_{a \in \text{roots}(p)} (X - a). \]

Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq theorem

(hp : p.Monic) (hroots : Multiset.card p.roots = p.natDegree) : (p.roots.map fun a => X - C a).prod = p

Full source

/-- A monic polynomial `p` that has as many roots as its degree
can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
theorem prod_multiset_X_sub_C_of_monic_of_roots_card_eq (hp : p.Monic)
    (hroots : Multiset.card p.roots = p.natDegree) : (p.roots.map fun a => X - C a).prod = p := by
  convert C_leadingCoeff_mul_prod_multiset_X_sub_C hroots
  rw [hp.leadingCoeff, C_1, one_mul]

Factorization of Monic Polynomial with Full Root Count: $p = \prod (X - a)$

Informal description

Let $p$ be a monic polynomial over a commutative ring $R$ such that the number of roots (counting multiplicities) equals its degree. Then $p$ can be expressed as the product of linear terms $(X - a)$ for each root $a$ in its multiset of roots, i.e., \[ p = \prod_{a \in \text{roots}(p)} (X - a). \]

Polynomial.Monic.isUnit_leadingCoeff_of_dvd theorem

{a p : R[X]} (hp : Monic p) (hap : a ∣ p) : IsUnit a.leadingCoeff

Full source

theorem Monic.isUnit_leadingCoeff_of_dvd {a p : R[X]} (hp : Monic p) (hap : a ∣ p) :
    IsUnit a.leadingCoeff :=
  isUnit_of_dvd_one (by simpa only [hp.leadingCoeff] using leadingCoeff_dvd_leadingCoeff hap)

Leading Coefficient of a Divisor of a Monic Polynomial is a Unit

Informal description

Let $R$ be a commutative ring and let $a, p \in R[X]$ be polynomials. If $p$ is monic and $a$ divides $p$, then the leading coefficient of $a$ is a unit in $R$.

Polynomial.Monic.irreducible_iff_degree_lt theorem

 {p : R[X]} (p_monic : Monic p) (p_1 : p ≠ 1) : Irreducible p ↔ ∀ q, degree q ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Full source

/-- To check a monic polynomial is irreducible, it suffices to check only for
divisors that have smaller degree.

See also: `Polynomial.Monic.irreducible_iff_natDegree`.
-/
theorem Monic.irreducible_iff_degree_lt {p : R[X]} (p_monic : Monic p) (p_1 : p ≠ 1) :
    IrreducibleIrreducible p ↔ ∀ q, degree q ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q := by
  simp only [p_monic.irreducible_iff_lt_natDegree_lt p_1, Finset.mem_Ioc, and_imp,
    natDegree_pos_iff_degree_pos, natDegree_le_iff_degree_le]
  constructor
  · rintro h q deg_le dvd
    by_contra q_unit
    have := degree_pos_of_not_isUnit_of_dvd_monic p_monic q_unit dvd
    have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd
    refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
    · rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
  · rintro h q _ deg_pos deg_le dvd
    exact deg_pos.ne' <| degree_eq_zero_of_isUnit (h q deg_le dvd)

Irreducibility Criterion for Monic Polynomials via Degree Bounds on Divisors

Informal description

Let $p$ be a monic polynomial over a commutative ring $R$ with $p \neq 1$. Then $p$ is irreducible if and only if for every polynomial $q$ of degree at most $\frac{1}{2}\deg(p)$, if $q$ divides $p$ then $q$ is a unit in $R[X]$.

Polynomial.le_rootMultiplicity_map theorem

{p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (a : A) : rootMultiplicity a p ≤ rootMultiplicity (f a) (p.map f)

Full source

theorem le_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hmap : mapmap f p ≠ 0) (a : A) :
    rootMultiplicity a p ≤ rootMultiplicity (f a) (p.map f) := by
  rw [le_rootMultiplicity_iff hmap]
  refine _root_.trans ?_ ((mapRingHom f).map_dvd (pow_rootMultiplicity_dvd p a))
  rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]

Inequality of Root Multiplicities Under Ring Homomorphisms: $\text{rootMultiplicity}(a, p) \leq \text{rootMultiplicity}(f(a), f(p))$

Informal description

Let $A$ and $B$ be commutative rings, $p \in A[X]$ a nonzero polynomial under the ring homomorphism $f : A \to B$ (i.e., $f(p) \neq 0$), and $a \in A$. Then the root multiplicity of $a$ in $p$ is less than or equal to the root multiplicity of $f(a)$ in $f(p)$.

Polynomial.count_map_roots theorem

 [IsDomain A] [DecidableEq B] {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (b : B) :
  (p.roots.map f).count b ≤ rootMultiplicity b (p.map f)

Full source

theorem count_map_roots [IsDomain A] [DecidableEq B] {p : A[X]} {f : A →+* B} (hmap : mapmap f p ≠ 0)
    (b : B) :
    (p.roots.map f).count b ≤ rootMultiplicity b (p.map f) := by
  rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ←
    Multiset.map_replicate fun a => X - C a]
  rw [← Multiset.filter_eq]
  refine
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_
  convert Polynomial.map_dvd f p.prod_multiset_X_sub_C_dvd
  simp only [Polynomial.map_multiset_prod, Multiset.map_map]
  congr; ext1
  simp only [Function.comp_apply, Polynomial.map_sub, map_X, map_C]

Upper Bound on Image Root Multiplicity: $\text{count}_b(f_*(\text{roots}(p))) \leq \text{rootMultiplicity}_b(f(p))$

Informal description

Let $A$ be an integral domain, $B$ a commutative ring with decidable equality, $p \in A[X]$ a polynomial, and $f \colon A \to B$ a ring homomorphism such that $f(p) \neq 0$. Then for any $b \in B$, the multiplicity of $b$ in the multiset obtained by applying $f$ to each root of $p$ is at most the root multiplicity of $b$ in $f(p)$. In symbols: $$ \text{count}_b(f_*(\text{roots}(p))) \leq \text{rootMultiplicity}_b(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.count_map_roots_of_injective theorem

 [IsDomain A] [DecidableEq B] (p : A[X]) {f : A →+* B} (hf : Function.Injective f) (b : B) :
  (p.roots.map f).count b ≤ rootMultiplicity b (p.map f)

Full source

theorem count_map_roots_of_injective [IsDomain A] [DecidableEq B] (p : A[X]) {f : A →+* B}
    (hf : Function.Injective f) (b : B) :
    (p.roots.map f).count b ≤ rootMultiplicity b (p.map f) := by
  by_cases hp0 : p = 0
  · simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero,
      rootMultiplicity_zero, le_refl]
  · exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b

Upper Bound on Image Root Multiplicity for Injective Homomorphisms: $\text{count}_b(f_*(\text{roots}(p))) \leq \text{rootMultiplicity}_b(f(p))$

Informal description

Let $A$ be an integral domain, $B$ a commutative ring with decidable equality, $p \in A[X]$ a polynomial, and $f \colon A \to B$ an injective ring homomorphism. Then for any $b \in B$, the multiplicity of $b$ in the multiset obtained by applying $f$ to each root of $p$ is at most the root multiplicity of $b$ in $f(p)$. In symbols: $$ \text{count}_b(f_*(\text{roots}(p))) \leq \text{rootMultiplicity}_b(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.map_roots_le theorem

[IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) : p.roots.map f ≤ (p.map f).roots

Full source

theorem map_roots_le [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
    p.roots.map f ≤ (p.map f).roots := by
  classical
  exact Multiset.le_iff_count.2 fun b => by
    rw [count_roots]
    apply count_map_roots h

Image of Roots Under Ring Homomorphism is Submultiset of Roots

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a polynomial, and $f \colon A \to B$ a ring homomorphism such that $f(p) \neq 0$. Then the multiset obtained by applying $f$ to each root of $p$ is a submultiset of the roots of $f(p)$. In symbols: $$ f_*(\mathrm{roots}(p)) \leq \mathrm{roots}(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.map_roots_le_of_injective theorem

[IsDomain A] [IsDomain B] (p : A[X]) {f : A →+* B} (hf : Function.Injective f) : p.roots.map f ≤ (p.map f).roots

Full source

theorem map_roots_le_of_injective [IsDomain A] [IsDomain B] (p : A[X]) {f : A →+* B}
    (hf : Function.Injective f) : p.roots.map f ≤ (p.map f).roots := by
  by_cases hp0 : p = 0
  · simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]
  exact map_roots_le ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Image of Roots Under Injective Ring Homomorphism is Submultiset of Roots

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a polynomial, and $f \colon A \to B$ an injective ring homomorphism. Then the multiset obtained by applying $f$ to each root of $p$ is a submultiset of the roots of $f(p)$. In symbols: $$ f_*(\mathrm{roots}(p)) \leq \mathrm{roots}(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.card_roots_le_map theorem

 [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
  Multiset.card p.roots ≤ Multiset.card (p.map f).roots

Full source

theorem card_roots_le_map [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
    Multiset.card p.roots ≤ Multiset.card (p.map f).roots := by
  rw [← p.roots.card_map f]
  exact Multiset.card_le_card (map_roots_le h)

Cardinality Inequality for Roots Under Ring Homomorphism: $|\mathrm{roots}(p)| \leq |\mathrm{roots}(f(p))|$

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a nonzero polynomial, and $f \colon A \to B$ a ring homomorphism such that $f(p) \neq 0$. Then the number of roots of $p$ (counted with multiplicity) is less than or equal to the number of roots of $f(p)$. In symbols: $$ |\mathrm{roots}(p)| \leq |\mathrm{roots}(f(p))| $$

Polynomial.card_roots_le_map_of_injective theorem

 [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (hf : Function.Injective f) :
  Multiset.card p.roots ≤ Multiset.card (p.map f).roots

Full source

theorem card_roots_le_map_of_injective [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B}
    (hf : Function.Injective f) : Multiset.card p.roots ≤ Multiset.card (p.map f).roots := by
  by_cases hp0 : p = 0
  · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]
  exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Root Count Inequality Under Injective Ring Homomorphism: $|\mathrm{roots}(p)| \leq |\mathrm{roots}(f(p))|$

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a polynomial, and $f \colon A \to B$ an injective ring homomorphism. Then the number of roots of $p$ (counted with multiplicity) is less than or equal to the number of roots of $f(p)$. In symbols: $$ |\mathrm{roots}(p)| \leq |\mathrm{roots}(f(p))| $$

Polynomial.roots_map_of_injective_of_card_eq_natDegree theorem

 [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (hf : Function.Injective f)
  (hroots : Multiset.card p.roots = p.natDegree) : p.roots.map f = (p.map f).roots

Full source

theorem roots_map_of_injective_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]}
    {f : A →+* B} (hf : Function.Injective f) (hroots : Multiset.card p.roots = p.natDegree) :
    p.roots.map f = (p.map f).roots := by
  apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
  simpa only [Multiset.card_map, hroots] using (card_roots' _).trans natDegree_map_le

Equality of Root Multisets Under Injective Ring Homomorphism When Root Count Matches Degree

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a polynomial, and $f \colon A \to B$ an injective ring homomorphism. If the number of roots of $p$ (counted with multiplicities) equals the degree of $p$, then the multiset obtained by applying $f$ to each root of $p$ is exactly the multiset of roots of $f(p)$. In symbols: $$ f_*(\mathrm{roots}(p)) = \mathrm{roots}(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.roots_map_of_map_ne_zero_of_card_eq_natDegree theorem

 [IsDomain A] [IsDomain B] {p : A[X]} (f : A →+* B) (h : p.map f ≠ 0) (hroots : p.roots.card = p.natDegree) :
  p.roots.map f = (p.map f).roots

Full source

theorem roots_map_of_map_ne_zero_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]}
    (f : A →+* B) (h : p.map f ≠ 0) (hroots : p.roots.card = p.natDegree) :
    p.roots.map f = (p.map f).roots :=
  eq_of_le_of_card_le (map_roots_le h) <| by
    simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans natDegree_map_le

Equality of Root Multisets Under Ring Homomorphism When Root Count Matches Degree

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a polynomial, and $f \colon A \to B$ a ring homomorphism such that $f(p) \neq 0$. If the number of roots of $p$ (counted with multiplicities) equals the degree of $p$, then the multiset obtained by applying $f$ to each root of $p$ is exactly the multiset of roots of $f(p)$. In symbols: $$ f_*(\mathrm{roots}(p)) = \mathrm{roots}(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Polynomial.Monic.roots_map_of_card_eq_natDegree theorem

 [IsDomain A] [IsDomain B] {p : A[X]} (hm : p.Monic) (f : A →+* B) (hroots : p.roots.card = p.natDegree) :
  p.roots.map f = (p.map f).roots

Full source

theorem Monic.roots_map_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]} (hm : p.Monic)
    (f : A →+* B) (hroots : p.roots.card = p.natDegree) : p.roots.map f = (p.map f).roots :=
  roots_map_of_map_ne_zero_of_card_eq_natDegree f (map_monic_ne_zero hm) hroots

Root Multiset Preservation for Monic Polynomials Under Ring Homomorphism

Informal description

Let $A$ and $B$ be integral domains, $p \in A[X]$ a monic polynomial, and $f \colon A \to B$ a ring homomorphism. If the number of roots of $p$ (counted with multiplicities) equals the degree of $p$, then the multiset obtained by applying $f$ to each root of $p$ is exactly the multiset of roots of $f(p)$. In symbols: $$ f_*(\mathrm{roots}(p)) = \mathrm{roots}(f(p)) $$ where $f_*$ denotes the pushforward of $f$ applied to each element of the multiset.

Mathlib.Algebra.Polynomial.Roots

Main definitions

Main statements