Loogle!

Result

Found 124 declarations mentioning Polynomial.IsRoot.

• Polynomial.IsRoot 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) (a : R) : Prop
• Polynomial.IsRoot.decidable 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} [DecidableEq R] : Decidable (p.IsRoot a)
• Polynomial.IsRoot.eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} (h : p.IsRoot x) : Polynomial.eval x p = 0
• Polynomial.IsRoot.def 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : p.IsRoot a ↔ Polynomial.eval a p = 0
• Polynomial.isRoot_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] {p q : Polynomial R} {r : R} : (p.comp q).IsRoot r ↔ p.IsRoot (Polynomial.eval r q)
• Polynomial.root_mul_left_of_isRoot 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [CommSemiring R] (p : Polynomial R) {q : Polynomial R} : q.IsRoot a → (p * q).IsRoot a
• Polynomial.root_mul_right_of_isRoot 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [CommSemiring R] {p : Polynomial R} (q : Polynomial R) : p.IsRoot a → (p * q).IsRoot a
• Polynomial.not_isRoot_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] (r a : R) (hr : r ≠ 0) : ¬(Polynomial.C r).IsRoot a
• Polynomial.isRoot_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_2} [CommSemiring R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R) : (∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x
• Polynomial.IsRoot.dvd 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] {p q : Polynomial R} {x : R} (h : p.IsRoot x) (hpq : p ∣ q) : q.IsRoot x
• Polynomial.root_or_root_of_root_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R] (h : (p * q).IsRoot a) : p.IsRoot a ∨ q.IsRoot a
• Polynomial.root_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R] : (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
• Polynomial.root_X_sub_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a b : R} [Ring R] : (Polynomial.X - Polynomial.C a).IsRoot b ↔ a = b
• Polynomial.coeff_zero_eq_zero_of_zero_isRoot 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.IsRoot 0 → p.coeff 0 = 0
• Polynomial.zero_isRoot_of_coeff_zero_eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff 0 = 0 → p.IsRoot 0
• Polynomial.zero_isRoot_iff_coeff_zero_eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.IsRoot 0 ↔ p.coeff 0 = 0
• Polynomial.IsRoot.map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R} (h : p.IsRoot x) : (Polynomial.map f p).IsRoot (f x)
• Polynomial.IsRoot.of_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {S : Type v} [CommSemiring S] {R : Type u_1} [Ring R] {f : R →+* S} {x : R} {p : Polynomial R} (h : (Polynomial.map f p).IsRoot (f x)) (hf : Function.Injective ⇑f) : p.IsRoot x
• Polynomial.isRoot_map_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {S : Type v} [CommSemiring S] {R : Type u_1} [CommRing R] {f : R →+* S} {x : R} {p : Polynomial R} (hf : Function.Injective ⇑f) : (Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x
• Polynomial.isRoot_of_eval₂_map_eq_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {r : R} : Polynomial.eval₂ f (f r) p = 0 → p.IsRoot r
• Polynomial.dvd_term_of_isRoot_of_dvd_terms 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [CommRing S] {r p : S} {f : Polynomial S} (i : ℕ) (hr : f.IsRoot r) (h : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i
• Polynomial.isRoot_of_aeval_algebraMap_eq_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} {r : R} (hr : (Polynomial.aeval ((algebraMap R S) r)) p = 0) : p.IsRoot r
• Polynomial.subsingleton_isRoot_of_natDegree_eq_one 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p : Polynomial R} [IsLeftCancelMulZero R] (h : p.natDegree = 1) : {x | p.IsRoot x}.Subsingleton
• Polynomial.degree_pos_of_root 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (h : p.IsRoot a) : 0 < p.degree
• Polynomial.rootMultiplicity_eq_zero 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} {x : R} (h : ¬p.IsRoot x) : Polynomial.rootMultiplicity x p = 0
• Polynomial.IsRoot.dvd_coeff_zero 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} {x : R} (h : p.IsRoot x) : x ∣ p.coeff 0
• Irreducible.subsingleton_isRoot 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) : {x | p.IsRoot x}.Subsingleton
• Irreducible.not_isRoot_of_natDegree_ne_one 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : R} : ¬p.IsRoot x
• Polynomial.rootMultiplicity_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} {x : R} : Polynomial.rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0
• Polynomial.rootMultiplicity_pos 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} (hp : p ≠ 0) {x : R} : 0 < Polynomial.rootMultiplicity x p ↔ p.IsRoot x
• Polynomial.rootMultiplicity_pos' 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} {x : R} : 0 < Polynomial.rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
• Polynomial.degree_eq_one_of_irreducible_of_root 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) {x : R} (hx : p.IsRoot x) : p.degree = 1
• Irreducible.isRoot_eq_bot_of_natDegree_ne_one 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.IsRoot = ⊥
• Polynomial.dvd_iff_isRoot 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {a : R} [CommRing R] {p : Polynomial R} : Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a
• Polynomial.mul_divByMonic_eq_iff_isRoot 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {a : R} [CommRing R] {p : Polynomial R} : (Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
• 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.eq_zero_of_infinite_isRoot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (h : {x | p.IsRoot x}.Infinite) : p = 0
• Polynomial.finite_setOfPred_isRoot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : {x | p.IsRoot x}.Finite
• Polynomial.finite_setOf_isRoot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : {x | p.IsRoot x}.Finite
• Polynomial.eventually_cofinite_not_isRoot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : ∀ᶠ (x : R) in Filter.cofinite, ¬p.IsRoot x
• 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.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.exists_max_root 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p ≠ 0) : ∃ x₀, ∀ (x : R), p.IsRoot x → x ≤ x₀
• Polynomial.exists_min_root 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p ≠ 0) : ∃ x₀, ∀ (x : R), p.IsRoot x → x₀ ≤ x
• 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.exists_root_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p : Polynomial R} (h : p.degree = 1) : ∃ x, p.IsRoot x
• Polynomial.isRoot_gcd_iff_isRoot_left_right 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] [DecidableEq R] {f g : Polynomial R} {α : R} : (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α
• Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (hn : n < Polynomial.rootMultiplicity t p) : ((⇑Polynomial.derivative)^[n] p).IsRoot t
• Polynomial.derivative_rootMultiplicity_of_root 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) : Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
• Polynomial.one_lt_rootMultiplicity_iff_isRoot 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ p.IsRoot t ∧ (Polynomial.derivative p).IsRoot t
• Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ 1, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [GCDMonoid (Polynomial R)] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ (gcd p (Polynomial.derivative p)).IsRoot t
• Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) (hnzd : ↑(Polynomial.rootMultiplicity t p) ∈ nonZeroDivisors R) : Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.IsRoot.mul_div_eq 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {a : R} [Field R] {p : Polynomial R} : p.IsRoot a → (Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p
• Polynomial.mul_div_eq_iff_isRoot 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {a : R} [Field R] {p : Polynomial R} : (Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
• Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {f g : Polynomial R} (hf0 : f ≠ 0) (hfd : f ∣ Polynomial.derivative f * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a
• Polynomial.Splits.mem_range_of_isRoot 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) (hf0 : f ≠ 0) {i : R →+* S} {x : S} (hx : (Polynomial.map i f).IsRoot x) : x ∈ i.range
• Polynomial.Splits.mem_subfield_of_isRoot 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] (F : Subfield R) {f : Polynomial ↥F} (hf : f.Splits) (hf0 : f ≠ 0) {x : R} (hx : (Polynomial.map F.subtype f).IsRoot x) : x ∈ F
• mem_rootsOfUnity_iff_isRoot 📋 Mathlib.RingTheory.RootsOfUnity.Basic
  {R : Type u_4} [CommRing R] (k : ℕ) (ζ : Rˣ) : ζ ∈ rootsOfUnity k R ↔ (Polynomial.X ^ k - 1).IsRoot ↑ζ
• Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {𝓟 : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt 𝓟) {x : R} (hroot : f.IsRoot x) (hmo : f.Monic) (i : ℕ) : f.natDegree ≤ i → x ^ i ∈ 𝓟
• minpoly.root 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [IsDomain B] [Algebra A B] {x : B} (hx : IsIntegral A x) {y : A} (h : (minpoly A x).IsRoot y) : (algebraMap A B) y = x
• AdjoinRoot.isRoot_root 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] (f : Polynomial R) : (Polynomial.map (AdjoinRoot.of f) f).IsRoot (AdjoinRoot.root f)
• IsAlgClosed.exists_root 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] (p : Polynomial k) (hp : p.degree ≠ 0) : ∃ x, p.IsRoot x
• Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K} (hf0 : f ≠ 0) : (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g
• Module.End.hasEigenvalue_of_isRoot 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} [IsDomain R] [Module.Finite R M] (h : (minpoly R f).IsRoot μ) : f.HasEigenvalue μ
• Module.End.isRoot_of_hasEigenvalue 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] {f : Module.End R M} {μ : R} (h : f.HasEigenvalue μ) : (minpoly R f).IsRoot μ
• Module.End.hasEigenvalue_iff_isRoot 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M] : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ
• num_isRoot_scaleRoots_of_aeval_eq_zero 📋 Mathlib.RingTheory.Polynomial.RationalRoot
  {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDomain A] [UniqueFactorizationMonoid A] {p : Polynomial A} {x : K} (hr : (Polynomial.aeval x) p = 0) : (p.scaleRoots ↑(IsFractionRing.den A x)).IsRoot (IsFractionRing.num A x)
• LinearMap.not_hasEigenvalue_zero_tfae 📋 Mathlib.LinearAlgebra.Eigenspace.Zero
  {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, LinearMap.ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
• LinearMap.hasEigenvalue_zero_tfae 📋 Mathlib.LinearAlgebra.Eigenspace.Zero
  {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < LinearMap.ker φ, ∃ m, m ≠ 0 ∧ φ m = 0].TFAE
• LinearRecurrence.geom_sol_iff_root_charPoly 📋 Mathlib.Algebra.LinearRecurrence
  {R : Type u_1} [CommRing R] (E : LinearRecurrence R) (q : R) : (E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q
• IsSepClosed.exists_root 📋 Mathlib.FieldTheory.IsSepClosed
  {k : Type u} [Field k] [IsSepClosed k] (p : Polynomial k) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x, p.IsRoot x
• Real.Polynomial.isRoot_cos_pi_div_five 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : (4 • Polynomial.X ^ 2 - 2 • Polynomial.X - Polynomial.C 1).IsRoot (Real.cos (Real.pi / 5))
• Polynomial.irreducible_of_degree_le_three_of_not_isRoot 📋 Mathlib.Algebra.Polynomial.SpecificDegree
  {K : Type u_1} [Field K] {p : Polynomial K} (hdeg : p.natDegree ∈ Finset.Icc 1 3) (hnot : ∀ (x : K), ¬p.IsRoot x) : Irreducible p
• WeierstrassCurve.Affine.Point.isRoot_twoTorsionPolynomial_of_add_self 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
  {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} [DecidableEq F] {x y : F} (h : W.Nonsingular x y) (hP : WeierstrassCurve.Affine.Point.some x y h + WeierstrassCurve.Affine.Point.some x y h = 0) : (WeierstrassCurve.twoTorsionPolynomial W).toPoly.IsRoot x
• WeierstrassCurve.Affine.Point.isRoot_twoTorsionPolynomial_iff 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
  {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} [DecidableEq F] (h2 : NeZero 2) (hΔ : WeierstrassCurve.Δ W ≠ 0) (x : F) : (WeierstrassCurve.twoTorsionPolynomial W).toPoly.IsRoot x ↔ ∃ y, ∃ (h : W.Nonsingular x y), WeierstrassCurve.Affine.Point.some x y h + WeierstrassCurve.Affine.Point.some x y h = 0
• Complex.exists_root 📋 Mathlib.Analysis.Complex.Polynomial.Basic
  {f : Polynomial ℂ} (hf : 0 < f.degree) : ∃ z, f.IsRoot z
• Polynomial.isIntegral_coeff_of_factors 📋 Mathlib.RingTheory.Polynomial.IsIntegral
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial S) (hpmon : IsIntegral R p.leadingCoeff) (hp : p.Splits) (hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x) (i : ℕ) : IsIntegral R (p.coeff i)
• Matrix.mem_spectrum_of_isRoot_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {B : Matrix n n R} [Nontrivial R] {r : R} (hr : B.charpoly.IsRoot r) : r ∈ spectrum R B
• Matrix.mem_spectrum_iff_isRoot_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} {r : K} : r ∈ spectrum K A ↔ A.charpoly.IsRoot r
• Module.End.hasEigenvalue_iff_isRoot_charpoly 📋 Mathlib.LinearAlgebra.Eigenspace.Charpoly
  {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : Module.End R M) (μ : R) : f.HasEigenvalue μ ↔ (LinearMap.charpoly f).IsRoot μ
• Module.End.mem_spectrum_iff_isRoot_charpoly 📋 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) (μ : K) : μ ∈ spectrum K f ↔ (LinearMap.charpoly f).IsRoot μ
• IsPrimitiveRoot.isRoot_geom_sum 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} {k : ℕ} [CommRing R] [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) : (∑ i ∈ Finset.range k, Polynomial.X ^ i).IsRoot ζ
• IsPrimitiveRoot.isRoot 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) : (Polynomial.X ^ n - 1).IsRoot ζ
• IsPrimitiveRoot.isRoot_of_dvd 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] {n n' : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) : n ∣ n' → (Polynomial.X ^ n' - 1).IsRoot ζ
• Polynomial.coprime_of_root_cyclotomic 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
  {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : Fact (Nat.Prime p)] {a : ℕ} (hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)) : a.Coprime p
• Polynomial.orderOf_root_cyclotomic_dvd 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
  {n : ℕ} (hpos : 0 < n) {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (hroot : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)) : orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
• IsPrimitiveRoot.pow_isRoot_minpoly 📋 Mathlib.RingTheory.RootsOfUnity.Minpoly
  {n : ℕ} {K : Type u_1} [CommRing K] {μ : K} (h : IsPrimitiveRoot μ n) [IsDomain K] [CharZero K] {m : ℕ} (hcop : m.Coprime n) : (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
• IsPrimitiveRoot.isRoot_cyclotomic 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (hpos : 0 < n) {μ : R} (h : IsPrimitiveRoot μ n) : (Polynomial.cyclotomic n R).IsRoot μ
• Polynomial.isRoot_cyclotomic_iff_charZero 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {n : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] [CharZero R] {μ : R} (hn : 0 < n) : (Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
• Polynomial.isRoot_cyclotomic_iff 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [NeZero ↑n] {μ : R} : (Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
• Polynomial.isRoot_of_unity_of_root_cyclotomic 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {R : Type u_1} [CommRing R] {n : ℕ} {ζ : R} {i : ℕ} (hi : i ∈ n.divisors) (h : (Polynomial.cyclotomic i R).IsRoot ζ) : ζ ^ n = 1
• isRoot_of_unity_iff 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
  {n : ℕ} (h : 0 < n) (R : Type u_2) [CommRing R] [IsDomain R] {ζ : R} : ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (Polynomial.cyclotomic i R).IsRoot ζ
• Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP 📋 Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
  {m k p : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] [hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R} [NeZero ↑m] : (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
• IsCyclotomicExtension.zeta_isRoot 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n] : (Polynomial.cyclotomic n B).IsRoot (IsCyclotomicExtension.zeta n A B)
• Polynomial.eventually_atBot_not_isRoot 📋 Mathlib.Analysis.Polynomial.Basic
  {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) (hP : P ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atBot, ¬P.IsRoot x
• Polynomial.eventually_atTop_not_isRoot 📋 Mathlib.Analysis.Polynomial.Basic
  {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) (hP : P ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x
• Polynomial.IsRoot.norm_lt_cauchyBound 📋 Mathlib.Analysis.Polynomial.CauchyBound
  {K : Type u_1} [NormedDivisionRing K] {p : Polynomial K} (hp : p ≠ 0) {a : K} (h : p.IsRoot a) : ‖a‖₊ < p.cauchyBound
• Polynomial.eval_le_zero_of_roots_le_of_leadingCoeff_nonpos 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x) (hlc : P.leadingCoeff ≤ 0) : Polynomial.eval x P ≤ 0
• Polynomial.eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y < x) (hlc : P.leadingCoeff ≤ 0) : Polynomial.eval x P < 0
• Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonneg 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x) (hlc : 0 ≤ P.leadingCoeff) : 0 ≤ Polynomial.eval x P
• Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y < x) (hlc : 0 ≤ P.leadingCoeff) : 0 < Polynomial.eval x P
• Polynomial.negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y) (hlc : P.leadingCoeff ≤ 0) : ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P ≤ 0
• Polynomial.negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x < y) (hlc : P.leadingCoeff ≤ 0) : ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P < 0
• Polynomial.zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y) (hlc : 0 ≤ P.leadingCoeff) : 0 ≤ ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P
• Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg 📋 Mathlib.Analysis.Polynomial.Order
  {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x < y) (hlc : 0 ≤ P.leadingCoeff) : 0 < ↑↑(↑P.natDegree).negOnePow * Polynomial.eval x P
• Polynomial.Chebyshev.irrational_of_isRoot_T_real 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
  {n : ℕ} {x : ℝ} (hroot : (Polynomial.Chebyshev.T ℝ ↑n).IsRoot x) (hnz : x ≠ 0) : Irrational x
• IsRealClosed.exists_isRoot_of_odd_natDegree 📋 Mathlib.FieldTheory.IsRealClosed.Basic
  {R : Type u_1} {inst✝ : Field R} [self : IsRealClosed R] {f : Polynomial R} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x
• IsRealClosed.of_linearOrderedField 📋 Mathlib.FieldTheory.IsRealClosed.Basic
  {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x) (exists_isRoot_of_odd_natDegree : ∀ {f : Polynomial R}, Odd f.natDegree → ∃ x, f.IsRoot x) : IsRealClosed R
• IsRealClosed.mk 📋 Mathlib.FieldTheory.IsRealClosed.Basic
  {R : Type u_1} [Field R] [toIsSemireal : IsSemireal R] (isSquare_or_isSquare_neg : ∀ (x : R), IsSquare x ∨ IsSquare (-x)) (exists_isRoot_of_odd_natDegree : ∀ {f : Polynomial R}, Odd f.natDegree → ∃ x, f.IsRoot x) : IsRealClosed R
• HenselianLocalRing.is_henselian 📋 Mathlib.RingTheory.Henselian
  {R : Type u_1} {inst✝ : CommRing R} [self : HenselianLocalRing R] (f : Polynomial R) : f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal R → IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal R
• HenselianLocalRing.mk 📋 Mathlib.RingTheory.Henselian
  {R : Type u_1} [CommRing R] [toIsLocalRing : IsLocalRing R] (is_henselian : ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal R → IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal R) : HenselianLocalRing R
• HenselianRing.is_henselian 📋 Mathlib.RingTheory.Henselian
  {R : Type u_1} {inst✝ : CommRing R} {I : Ideal R} [self : HenselianRing R I] (f : Polynomial R) : f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ I → IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
• HenselianRing.mk 📋 Mathlib.RingTheory.Henselian
  {R : Type u_1} [CommRing R] {I : Ideal R} (jac : I ≤ ⊥.jacobson) (is_henselian : ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ I → IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I) : HenselianRing R I
• HenselianLocalRing.TFAE 📋 Mathlib.RingTheory.Henselian
  (R : Type u) [CommRing R] [IsLocalRing R] : [HenselianLocalRing R, ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : IsLocalRing.ResidueField R), (Polynomial.aeval a₀) f = 0 → (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (IsLocalRing.residue R) a = a₀, ∀ {K : Type u} [inst : Field K] (φ : R →+* K), Function.Surjective ⇑φ → ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : K), Polynomial.eval₂ φ a₀ f = 0 → Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
• WittVector.RecursionMain.root_exists 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ∃ b, (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot b
• WittVector.RecursionMain.succNthVal_spec 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)

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 69fae59