Loogle!

Result

Found 193 declarations mentioning Polynomial.roots.

• Polynomial.roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : Multiset R
• Polynomial.card_roots' 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : p.roots.card ≤ p.natDegree
• Polynomial.count_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) : Multiset.count a p.roots = Polynomial.rootMultiplicity a p
• Polynomial.isRoot_of_mem_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a ∈ p.roots) : p.IsRoot a
• Polynomial.roots_neg 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : (-p).roots = p.roots
• Polynomial.roots_X 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] : Polynomial.X.roots = {0}
• Polynomial.card_le_degree_of_subset_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {Z : Finset R} (h : Z.val ⊆ p.roots) : Z.card ≤ p.natDegree
• Polynomial.roots_one 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] : Polynomial.roots 1 = ∅
• Polynomial.roots_zero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] : Polynomial.roots 0 = 0
• Polynomial.card_roots_map_le_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_3} {B : Type u_4} [Semiring A] [CommRing B] [IsDomain B] {f : A →+* B} (p : Polynomial A) : (Polynomial.map f p).roots.card ≤ p.natDegree
• Polynomial.card_roots_le_one_of_irreducible 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hirr : Irreducible p) : p.roots.card ≤ 1
• Associated.roots_eq 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (h : Associated p q) : p.roots = q.roots
• Polynomial.ne_zero_of_mem_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a ∈ p.roots) : p ≠ 0
• Polynomial.aroots_def 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : p.aroots S = (Polynomial.map (algebraMap T S) p).roots
• Polynomial.mem_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : a ∈ p.roots ↔ p.IsRoot a
• Polynomial.roots_eq_zero_of_irreducible_of_natDegree_ne_one 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hirr : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.roots = 0
• Polynomial.mem_roots' 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} : a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a
• Polynomial.roots_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : (p.comp (-Polynomial.X)).roots = Multiset.map (fun x => -x) p.roots
• Polynomial.card_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp0 : p ≠ 0) : ↑p.roots.card ≤ p.degree
• Polynomial.card_roots_map_le_degree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_3} {B : Type u_4} [Semiring A] [CommRing B] [IsDomain B] {f : A →+* B} (p : Polynomial A) (hp0 : p ≠ 0) : ↑(Polynomial.map f p).roots.card ≤ p.degree
• Polynomial.roots_eq_of_degree_eq_card 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {S : Finset R} (hS : ∀ x ∈ S, Polynomial.eval x p = 0) (hcard : ↑S.card = p.degree) : p.roots = S.val
• Polynomial.roots_eq_zero_iff_isRoot_eq_bot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp0 : p ≠ 0) : p.roots = 0 ↔ p.IsRoot = ⊥
• Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} : p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥
• Polynomial.roots_ofMultiset 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) : (Polynomial.ofMultiset s).roots = s
• Polynomial.rightInverse_ofMultiset_roots 📋 Mathlib.Algebra.Polynomial.Roots
  (R : Type u) [CommRing R] [IsDomain R] : Function.RightInverse (⇑Polynomial.ofMultiset) Polynomial.roots
• Polynomial.roots_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (x : R) : (Polynomial.C x).roots = 0
• Polynomial.roots_multiset_prod 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (m : Multiset (Polynomial R)) : 0 ∉ m → m.prod.roots = m.bind Polynomial.roots
• Polynomial.roots_smul_nonzero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a ≠ 0) : (a • p).roots = p.roots
• Polynomial.roots_pow 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (n : ℕ) : (p ^ n).roots = n • p.roots
• Polynomial.roots_eq_of_natDegree_le_card_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {S : Finset R} (hS : ∀ x ∈ S, Polynomial.eval x p = 0) (hcard : p.natDegree ≤ S.card) (hp : p ≠ 0) : p.roots = S.val
• Polynomial.card_roots_le_map_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) : p.roots.card ≤ (Polynomial.map f p).roots.card
• Polynomial.roots_prod 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι) : s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => (f i).roots
• Polynomial.roots_list_prod 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (L : List (Polynomial R)) : 0 ∉ L → L.prod.roots = (↑L).bind Polynomial.roots
• Polynomial.card_roots_le_map 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : p.roots.card ≤ (Polynomial.map f p).roots.card
• Polynomial.roots_X_pow 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (n : ℕ) : (Polynomial.X ^ n).roots = n • {0}
• Polynomial.roots_eq_of_degree_le_card_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {S : Finset R} (hS : ∀ x ∈ S, Polynomial.eval x p = 0) (hcard : p.degree ≤ ↑S.card) (hp : p ≠ 0) : p.roots = S.val
• Polynomial.mem_roots_map_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [Semiring S] {p : Polynomial S} {f : S →+* R} (hf : Function.Injective ⇑f) {x : R} (hp : p ≠ 0) : x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0
• Polynomial.Monic.roots_map_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} (hm : p.Monic) (f : A →+* B) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.roots.le_of_dvd 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (h : q ≠ 0) : p ∣ q → p.roots ≤ q.roots
• Polynomial.roots_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (r : R) : (Polynomial.X - Polynomial.C r).roots = {r}
• Polynomial.bUnion_roots_finite 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ) {U : Set R} (h : U.Finite) : (⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite
• Polynomial.count_map_roots_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) (b : B) : Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
• Polynomial.count_map_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p ≠ 0) (b : B) : Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
• Polynomial.map_roots_le_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) : Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
• Polynomial.roots_mul 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots
• Polynomial.roots_C_mul 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a ≠ 0) : (Polynomial.C a * p).roots = p.roots
• Polynomial.roots_X_add_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (r : R) : (Polynomial.X + Polynomial.C r).roots = {-r}
• Polynomial.roots_prod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (s : Finset R) : (∏ a ∈ s, (Polynomial.X - Polynomial.C a)).roots = s.val
• Polynomial.map_roots_le 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
• Polynomial.roots_map_of_injective_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.roots_multiset_prod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.roots = s
• Polynomial.roots_map_of_map_ne_zero_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} (f : A →+* B) (h : Polynomial.map f p ≠ 0) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.card_roots_sub_C' 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < p.degree) : (p - Polynomial.C a).roots.card ≤ p.natDegree
• Polynomial.mem_roots_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a x : R} (hp0 : 0 < p.degree) : x ∈ (p - Polynomial.C a).roots ↔ Polynomial.eval x p = a
• Polynomial.card_roots_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < p.degree) : ↑(p - Polynomial.C a).roots.card ≤ p.degree
• Polynomial.mem_roots_iff_aeval_eq_zero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {x : R} (w : p ≠ 0) : x ∈ p.roots ↔ (Polynomial.aeval x) p = 0
• Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p.Monic) (hroots : p.roots.card = p.natDegree) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
• Polynomial.card_roots_X_pow_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {n : ℕ} (hn : 0 < n) (a : R) : (Polynomial.X ^ n - Polynomial.C a).roots.card ≤ n
• Polynomial.roots_def 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) [Decidable (p = 0)] : p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
• Polynomial.prod_multiset_X_sub_C_dvd 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod ∣ p
• Polynomial.filter_roots_map_range_eq_map_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {f : A →+* B} [DecidablePred fun x => x ∈ f.range] (hf : Function.Injective ⇑f) (p : Polynomial A) : Multiset.filter (fun x => x ∈ f.range) (Polynomial.map f p).roots = Multiset.map (⇑f) p.roots
• Polynomial.mem_roots_sub_C' 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a x : R} : x ∈ (p - Polynomial.C a).roots ↔ p ≠ Polynomial.C a ∧ Polynomial.eval x p = a
• Polynomial.roots_monomial 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a ≠ 0) (n : ℕ) : ((Polynomial.monomial n) a).roots = n • {0}
• Polynomial.roots_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a ≠ 0) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).roots = n • {0}
• Multiset.prod_X_sub_C_dvd_iff_le_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) (s : Multiset R) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod ∣ p ↔ s ≤ p.roots
• Polynomial.exists_prod_multiset_X_sub_C_mul 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) : ∃ q, (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
• Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : p.roots.card = p.natDegree) : Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
• Polynomial.roots_C_mul_X_sub_C_of_IsUnit 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (b : R) (a : Rˣ) : (Polynomial.C ↑a * Polynomial.X - Polynomial.C b).roots = {↑a⁻¹ * b}
• Polynomial.map_roots_comp_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (a b : R) (ha : IsUnit a) : Multiset.map (fun x => a * x + b) (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = p.roots
• Polynomial.roots_comp_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (a b : R) (ha : IsUnit a) : (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = Multiset.map (fun x => Ring.inverse a * (x - b)) p.roots
• Polynomial.roots_C_mul_X_add_C_of_IsUnit 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (b : R) (a : Rˣ) : (Polynomial.C ↑a * Polynomial.X + Polynomial.C b).roots = {-(↑a⁻¹ * b)}
• Polynomial.prod_multiset_root_eq_finset_root 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} [DecidableEq R] : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = ∏ a ∈ p.roots.toFinset, (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p
• Polynomial.roots_normalize 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} : (normalize p).roots = p.roots
• Polynomial.mem_roots_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) : x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0
• Polynomial.roots_degree_eq_one 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p : Polynomial R} (h : p.degree = 1) : p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}
• Polynomial.roots_C_mul_X_sub_C 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {a : R} [Field R] (b : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X - Polynomial.C b).roots = {a⁻¹ * b}
• Polynomial.roots_C_mul_X_add_C 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {a : R} [Field R] (b : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).roots = {-(a⁻¹ * b)}
• Polynomial.Splits.natDegree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.natDegree = f.roots.card
• Polynomial.splits_iff_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : f.Splits ↔ f.roots.card = f.natDegree
• Polynomial.Splits.roots_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f.natDegree ≠ 0) : f.roots ≠ 0
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum
• Polynomial.Splits.eval_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) (x : R) : Polynomial.eval x f = (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.Splits.degree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f ≠ 0) : f.degree = ↑f.roots.card
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.nextCoeff = -f.leadingCoeff * f.roots.sum
• Polynomial.Splits.eval_eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (x : R) : Polynomial.eval x f = f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.map_sub_sprod_roots_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.Splits.roots_map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) (i : R →+* S) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.Splits.of_splits_map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (i : R →+* S) (hf : (Polynomial.map i f).Splits) (hi : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : f.Splits
• Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod
• Polynomial.Splits.roots_map_of_injective 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] (hf : f.Splits) {i : R →+* S} (hi : Function.Injective ⇑i) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.Splits.roots_map_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) {φ : R →+* S} (hφ : Polynomial.map φ f ≠ 0) : (Polynomial.map φ f).roots = Multiset.map (⇑φ) f.roots
• Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod
• Polynomial.Splits.of_splits_map_of_injective 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] {i : R →+* S} (hi : Function.Injective ⇑i) (hf : (Polynomial.map i f).Splits) : (∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) → f.Splits
• Polynomial.Splits.dvd_of_roots_le_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hp : f.Splits) (hp0 : f ≠ 0) (hq : f.roots ≤ g.roots) : f ∣ g
• Polynomial.map_sub_roots_sprod_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (g.roots ×ˢ s)).prod = (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.Splits.eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.mem_lift_of_roots_mem_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) {S : Type u_4} [Ring S] (i : S →+* R) (hr : ∀ a ∈ f.roots, a ∈ i.range) : f ∈ Polynomial.lifts i
• Polynomial.Splits.dvd_iff_roots_le_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hf0 : f ≠ 0) (hg0 : g ≠ 0) : f ∣ g ↔ f.roots ≤ g.roots
• Polynomial.Splits.eq_X_sub_C_of_single_root 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) {x : R} (hr : f.roots = {x}) : f = Polynomial.C f.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Polynomial.Splits.eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.eval_root_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : Polynomial.eval x (Polynomial.derivative f) = (Multiset.map (fun x_1 => x - x_1) (f.roots.erase x)).prod
• Polynomial.Splits.eval_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : Polynomial.eval x (Polynomial.derivative f) = f.leadingCoeff * (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
• Polynomial.Splits.eval_derivative_div_eval_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) / Polynomial.eval x f = (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Polynomial.Splits.eval_derivative_eq_eval_mul_sum 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) = Polynomial.eval x f * (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Polynomial.roots_scaleRoots 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) {r : R} (hr : IsUnit r) : (p.scaleRoots r).roots = Multiset.map (fun x => r * x) p.roots
• Cubic.map_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} {P : Cubic R} [CommRing R] [CommRing S] {φ : R →+* S} [IsDomain S] : (Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
• Polynomial.nodup_roots 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hsep : p.Separable) : p.roots.Nodup
• Polynomial.count_roots_le_one 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} (hsep : p.Separable) (x : R) : Multiset.count x p.roots ≤ 1
• Polynomial.nodup_roots_iff_of_splits 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {f : Polynomial F} (hf : f ≠ 0) (h : f.Splits) : f.roots.Nodup ↔ f.Separable
• Polynomial.eq_X_sub_C_of_separable_of_root_eq 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] {i : F →+* K} {x : F} {h : Polynomial F} (h_sep : h.Separable) (h_root : Polynomial.eval x h = 0) (h_splits : (Polynomial.map i h).Splits) (h_roots : ∀ y ∈ (Polynomial.map i h).roots, y = i x) : h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Polynomial.rootsExpandToRoots 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : ↥((Polynomial.expand R p) f).roots.toFinset ↪ ↥f.roots.toFinset
• Polynomial.rootsExpandEquivRoots 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] : ↥((Polynomial.expand R p) f).roots.toFinset ≃ ↥f.roots.toFinset
• Polynomial.rootsExpandPowToRoots 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset ↪ ↥f.roots.toFinset
• Polynomial.rootsExpandPowEquivRoots 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (n : ℕ) : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset ≃ ↥f.roots.toFinset
• Polynomial.roots_expand_image_frobenius_subset 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset ⊆ f.roots.toFinset
• Polynomial.roots_expand_image_frobenius 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] : Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset = f.roots.toFinset
• Polynomial.roots_expand_pow_image_iterateFrobenius_subset 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] : Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset
• Polynomial.roots_expand_map_frobenius_le 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) : Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots ≤ p • f.roots
• Polynomial.roots_expand_image_iterateFrobenius 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] : Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
• Polynomial.roots_expand_map_frobenius 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots = p • f.roots
• Polynomial.roots_expand_pow_map_iterateFrobenius_le 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) : Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots ≤ p ^ n • f.roots
• Polynomial.roots_expand_pow_map_iterateFrobenius 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • f.roots
• Polynomial.roots_expand 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : ((Polynomial.expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
• Polynomial.roots_X_pow_char_sub_C 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} : (Polynomial.X ^ p - Polynomial.C y).roots = p • {(frobeniusEquiv R p).symm y}
• Polynomial.roots_expand_pow 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} [PerfectRing R p] : ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
• Polynomial.roots_X_pow_char_pow_sub_C 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} : (Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
• Polynomial.roots_X_pow_char_sub_C_pow 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} {m : ℕ} : ((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
• Polynomial.roots_X_pow_char_pow_sub_C_pow 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] {p n : ℕ} [ExpChar R p] [PerfectRing R p] {y : R} {m : ℕ} : ((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}
• Polynomial.rootsExpandToRoots_apply 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : ↥((Polynomial.expand R p) f).roots.toFinset) : ↑((Polynomial.rootsExpandToRoots p f) x) = ↑x ^ p
• Polynomial.rootsExpandPowToRoots_apply 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p n : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset) : ↑((Polynomial.rootsExpandPowToRoots p n f) x) = ↑x ^ p ^ n
• Polynomial.rootsExpandEquivRoots_apply 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (x : ↥((Polynomial.expand R p) f).roots.toFinset) : ↑((Polynomial.rootsExpandEquivRoots p f) x) = ↑x ^ p
• Polynomial.rootsExpandPowEquivRoots_apply 📋 Mathlib.FieldTheory.Perfect
  {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] [PerfectRing R p] (n : ℕ) (x : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset) : ↑((Polynomial.rootsExpandPowEquivRoots p f n) x) = ↑x ^ p ^ n
• IsAlgClosed.card_roots_eq_natDegree 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots.card = p.natDegree
• IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.natDegree = 0
• IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] (f : A →+* B) {p : Polynomial A} (h : IsUnit p.leadingCoeff) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.roots_eq_zero_iff_degree_nonpos 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.degree ≤ 0
• IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Ring A] [IsSimpleRing A] [Field B] [IsAlgClosed B] (f : A →+* B) (p : Polynomial A) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.card_roots_map_eq_natDegree_of_injective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} (p : Polynomial A) (hf : Function.Injective ⇑f) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} {p : Polynomial A} (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.associated_iff_roots_eq_roots 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : Associated p q ↔ p.roots = q.roots
• IsAlgClosed.roots_eq_zero_iff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
• IsAlgClosed.dvd_iff_roots_le_roots 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : p ∣ q ↔ p.roots ≤ q.roots
• spectrum.exists_mem_of_not_isUnit_aeval_prod 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] {p : Polynomial R} {a : A} (h : ¬IsUnit ((Polynomial.aeval a) (Multiset.map (fun x => Polynomial.X - Polynomial.C x) p.roots).prod)) : ∃ k ∈ spectrum R a, Polynomial.eval k p = 0
• AlgebraicClosure.finEquivRoots 📋 Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
  {k : Type u} [Field k] {K : Type u_1} [Field K] [DecidableEq K] {i : k →+* K} {f : AlgebraicClosure.Monics k} (hf : (Polynomial.map i ↑f).Splits) : Fin (↑f).natDegree ≃ ↥(Polynomial.map i ↑f).roots.toEnumFinset
• Field.primitive_element_inf_aux_exists_c 📋 Mathlib.FieldTheory.PrimitiveElement
  {F : Type u_1} [Field F] [Infinite F] {E : Type u_2} [Field E] (ϕ : F →+* E) (α β : E) (f g : Polynomial F) : ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
• IsSepClosed.roots_eq_zero_iff 📋 Mathlib.FieldTheory.IsSepClosed
  {k : Type u} [Field k] [IsSepClosed k] {p : Polynomial k} (hsep : p.Separable) : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
• Polynomial.roots_countP_pos_le_signVariations 📋 Mathlib.Algebra.Polynomial.RuleOfSigns
  {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (P : Polynomial R) : Multiset.countP (fun x => 0 < x) P.roots ≤ P.signVariations
• Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three 📋 Mathlib.Algebra.Polynomial.SpecificDegree
  {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p.Monic) (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0
• Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three 📋 Mathlib.Algebra.Polynomial.SpecificDegree
  {K : Type u_1} [Field K] {p : Polynomial K} (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0
• Polynomial.coeff_eq_esymm_roots_of_card 📋 Mathlib.RingTheory.Polynomial.Vieta
  {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : p.roots.card = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) : p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
• Polynomial.coeff_eq_esymm_roots_of_splits 📋 Mathlib.RingTheory.Polynomial.Vieta
  {F : Type u_2} [Field F] {p : Polynomial F} (hsplit : p.Splits) {k : ℕ} (h : k ≤ p.natDegree) : p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
• Polynomial.eq_one_of_roots_le 📋 Mathlib.Topology.Algebra.Polynomial
  {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ} (hB : B < 0) (h1 : p.Monic) (h2 : (Polynomial.map f p).Splits) (h3 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) : p = 1
• Polynomial.coeff_le_of_roots_le 📋 Mathlib.Topology.Algebra.Polynomial
  {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.Monic) (h2 : (Polynomial.map f p).Splits) (h3 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) : ‖(Polynomial.map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)
• Polynomial.coeff_bdd_of_roots_le 📋 Mathlib.Topology.Algebra.Polynomial
  {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {B : ℝ} {d : ℕ} (f : F →+* K) {p : Polynomial F} (h1 : p.Monic) (h2 : (Polynomial.map f p).Splits) (h3 : p.natDegree ≤ d) (h4 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) (i : ℕ) : ‖(Polynomial.map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
• FiniteField.roots_X_pow_card_sub_X 📋 Mathlib.FieldTheory.Finite.Basic
  (K : Type u_1) [Field K] [Fintype K] : (Polynomial.X ^ Fintype.card K - Polynomial.X).roots = Finset.univ.val
• Subfield.roots_X_pow_char_sub_X_bot 📋 Mathlib.FieldTheory.Finite.Basic
  (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] : (Polynomial.X ^ p - Polynomial.X).roots = Finset.univ.val
• Polynomial.resultant_eq_prod_eval 📋 Mathlib.RingTheory.Polynomial.Resultant.Basic
  {R : Type u_1} [CommRing R] [IsDomain R] (f g : Polynomial R) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits) : f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x => Polynomial.eval x g) f.roots).prod
• Polynomial.resultant_eq_prod_roots_sub 📋 Mathlib.RingTheory.Polynomial.Resultant.Basic
  {K : Type u_3} [Field K] (f g : Polynomial K) (hf : f.Monic) (hg : g.Monic) (hf' : f.Splits) (hg' : g.Splits) : f.resultant g = (Multiset.map (fun ij => ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
• Polynomial.card_roots_le_derivative 📋 Mathlib.Analysis.Calculus.LocalExtr.Polynomial
  (p : Polynomial ℝ) : p.roots.card ≤ (Polynomial.derivative p).roots.card + 1
• Polynomial.card_roots_toFinset_le_derivative 📋 Mathlib.Analysis.Calculus.LocalExtr.Polynomial
  (p : Polynomial ℝ) : p.roots.toFinset.card ≤ (Polynomial.derivative p).roots.toFinset.card + 1
• Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ 📋 Mathlib.Analysis.Calculus.LocalExtr.Polynomial
  (p : Polynomial ℝ) : p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
• Polynomial.card_roots_toFinset_le_card_roots_derivative_sdiff_roots_succ 📋 Mathlib.Analysis.Calculus.LocalExtr.Polynomial
  (p : Polynomial ℝ) : p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
• Polynomial.sum_derivRootWeight_pos 📋 Mathlib.Analysis.Complex.Polynomial.GaussLucas
  {P : Polynomial ℂ} (hP : 0 < P.degree) (z : ℂ) : 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w
• Polynomial.eq_centerMass_of_eval_derivative_eq_zero 📋 Mathlib.Analysis.Complex.Polynomial.GaussLucas
  {P : Polynomial ℂ} {z : ℂ} (hP : 0 < P.degree) (hz : Polynomial.eval z (Polynomial.derivative P) = 0) : z = P.roots.toFinset.centerMass (P.derivRootWeight z) id
• Matrix.det_eq_prod_roots_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K] (A : Matrix n n K) [IsAlgClosed K] : A.det = A.charpoly.roots.prod
• Matrix.det_eq_prod_roots_charpoly_of_splits 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {B : Matrix n n R} [IsDomain R] (hAps : B.charpoly.Splits) : B.det = B.charpoly.roots.prod
• Matrix.trace_eq_sum_roots_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K] (A : Matrix n n K) [IsAlgClosed K] : A.trace = A.charpoly.roots.sum
• Matrix.trace_eq_sum_roots_charpoly_of_splits 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {B : Matrix n n R} [IsDomain R] (hAps : B.charpoly.Splits) : B.trace = B.charpoly.roots.sum
• Module.End.det_eq_prod_roots_charpoly_of_splits 📋 Mathlib.LinearAlgebra.Eigenspace.Charpoly
  {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] [Module.Finite K V] {f : Module.End K V} (h : (LinearMap.charpoly f).Splits) : LinearMap.det f = (LinearMap.charpoly f).roots.prod
• Module.End.trace_eq_sum_roots_charpoly_of_splits 📋 Mathlib.LinearAlgebra.Eigenspace.Charpoly
  {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] [Module.Finite K V] {f : Module.End K V} (h : (LinearMap.charpoly f).Splits) : (LinearMap.trace K V) f = (LinearMap.charpoly f).roots.sum
• LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues 📋 Mathlib.Analysis.InnerProductSpace.Spectrum
  {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : T.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) Finset.univ.val
• LinearMap.IsSymmetric.sort_roots_charpoly_eq_eigenvalues 📋 Mathlib.Analysis.InnerProductSpace.Spectrum
  {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : ((Multiset.map (⇑RCLike.re) T.charpoly.roots).sort fun x1 x2 => x1 ≥ x2) = List.ofFn (hT.eigenvalues hn)
• Matrix.IsHermitian.roots_charpoly_eq_eigenvalues 📋 Mathlib.Analysis.Matrix.Spectrum
  {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val
• Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀ 📋 Mathlib.Analysis.Matrix.Spectrum
  {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val
• Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀ 📋 Mathlib.Analysis.Matrix.Spectrum
  {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : ((Multiset.map (⇑RCLike.re) A.charpoly.roots).sort fun x1 x2 => x1 ≥ x2) = List.ofFn hA.eigenvalues₀
• Polynomial.roots_of_cyclotomic 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
  (n : ℕ) (R : Type u_2) [CommRing R] [IsDomain R] : (Polynomial.cyclotomic' n R).roots = (primitiveRoots n R).val
• IsPrimitiveRoot.is_roots_of_minpoly 📋 Mathlib.RingTheory.RootsOfUnity.Minpoly
  {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] [DecidableEq K] : primitiveRoots n K ⊆ (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
• Polynomial.roots_cyclotomic_nodup 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : (Polynomial.cyclotomic n R).roots.Nodup
• Polynomial.cyclotomic.roots_eq_primitiveRoots_val 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : (Polynomial.cyclotomic n R).roots = (primitiveRoots n R).val
• Polynomial.cyclotomic.roots_to_finset_eq_primitiveRoots 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] : { val := (Polynomial.cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R
• Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt 📋 Mathlib.Analysis.Normed.Field.Approximation
  {K : Type u_1} [NormedField K] {f g : Polynomial K} {ε : ℝ} (hε : 0 < ε) {a : K} (ha : Polynomial.eval a f = 0) (hfm : f.Monic) (hgm : g.Monic) (hdeg : g.natDegree = f.natDegree) (hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε) (hg : g.Splits) : ∃ b ∈ g.roots, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
• spectralNorm.spectralMulAlgNorm_eq_of_mem_roots 📋 Mathlib.Analysis.Normed.Unbundled.SpectralNorm
  (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) {E : Type u_2} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic K E] {a : E} (ha : a ∈ ((Polynomial.mapAlg K E) (minpoly K x)).roots) : (spectralMulAlgNorm K E) a = (spectralMulAlgNorm K E) ((algebraMap L E) x)
• spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots 📋 Mathlib.Analysis.Normed.Unbundled.SpectralNorm
  (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) {E : Type u_2} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Polynomial.IsSplittingField L E ((Polynomial.mapAlg K L) (minpoly K x))] [Algebra.IsAlgebraic K E] : (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree = (spectralMulAlgNorm K E) ((Polynomial.mapAlg K E) (minpoly K x)).roots.prod
• Polynomial.one_le_prod_max_one_norm_roots 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  (p : Polynomial ℂ) : 1 ≤ (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod
• Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  (p : Polynomial ℂ) : p.logMahlerMeasure = Real.log ‖p.leadingCoeff‖ + (Multiset.map (fun a => ‖a‖.posLog) p.roots).sum
• Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  (p : Polynomial ℂ) : p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod
• Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  {p : Polynomial ℂ} (hlc : 1 ≤ ‖p.leadingCoeff‖) : (Multiset.map (fun a => max 1 ‖a‖) p.roots).prod ≤ p.mahlerMeasure
• Polynomial.Chebyshev.roots_U_real 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
  (n : ℕ) : (Polynomial.Chebyshev.U ℝ ↑n).roots = (Finset.image (fun k => Real.cos ((↑k + 1) * Real.pi / (↑n + 1))) (Finset.range n)).val
• Polynomial.Chebyshev.roots_T_real 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
  (n : ℕ) : (Polynomial.Chebyshev.T ℝ ↑n).roots = (Finset.image (fun k => Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Finset.range n)).val
• Polynomial.eq_mul_mul_of_roots_quadratic_eq_pair 📋 Mathlib.RingTheory.Polynomial.SmallDegreeVieta
  {R : Type u_1} [CommRing R] [IsDomain R] {a b c x1 x2 : R} (hroots : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2}) : c = a * x1 * x2
• Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair 📋 Mathlib.RingTheory.Polynomial.SmallDegreeVieta
  {R : Type u_1} [CommRing R] [IsDomain R] {a b c x1 x2 : R} (hroots : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2}) : b = -a * (x1 + x2)
• Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero 📋 Mathlib.RingTheory.Polynomial.SmallDegreeVieta
  {R : Type u_1} [CommRing R] [IsDomain R] {a b c x1 x2 : R} (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} ↔ b = -a * (x1 + x2) ∧ c = a * x1 * x2
• Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero' 📋 Mathlib.RingTheory.Polynomial.SmallDegreeVieta
  {R : Type u_1} [Field R] {a b c x1 x2 : R} (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c