ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b c : α<VAR>hb : b ≤ c<VAR>ha : c * a ≤ c<GOAL>b * a∗ ≤ c
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b c : α<VAR>hb : b ≤ c<VAR>ha : a * c ≤ c<GOAL>a∗ * b ≤ c
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b : α<VAR>hb : 1 ≤ b<GOAL>b * a ≤ b → a∗ ≤ b
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b : α<VAR>hb : 1 ≤ b<GOAL>a * b ≤ b → a∗ ≤ b
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a ≤ a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<GOAL>Monotone KStar.kstar
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a∗ = 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>KleeneAlgebra α<GOAL>0∗ = 1
<VAR>α : Type u_1<VAR>KleeneAlgebra α<GOAL>1∗ = 1
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a∗ * a∗ = a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a∗ = a ↔ a * a = a ∧ 1 ≤ a
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a∗∗ = a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<VAR>n : ℕ<GOAL>a ^ n ≤ a∗
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>KleeneAlgebra α<VAR>KleeneAlgebra β<VAR>a : α × β<GOAL>a∗ = (a.1∗, a.2∗)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>KleeneAlgebra α<VAR>KleeneAlgebra β<VAR>a : α × β<GOAL>a∗.1 = a.1∗
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>KleeneAlgebra α<VAR>KleeneAlgebra β<VAR>a : α × β<GOAL>a∗.2 = a.2∗
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → KleeneAlgebra (π i)<VAR>a : (i : ι) → π i<GOAL>a∗ = fun i => (a i)∗
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → KleeneAlgebra (π i)<VAR>a : (i : ι) → π i<VAR>i : ι<GOAL>a∗ i = (a i)∗
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<VAR>p : Polynomial R<VAR>Decidable (p = 0)<GOAL>p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.roots 0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp0 : p ≠ 0<GOAL>↑(Multiset.card p.roots) ≤ p.degree
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>Multiset.card p.roots ≤ p.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>a : R<VAR>hp0 : 0 < p.degree<GOAL>↑(Multiset.card (p - Polynomial.C a).roots) ≤ p.degree
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>a : R<VAR>hp0 : 0 < p.degree<GOAL>Multiset.card (p - Polynomial.C a).roots ≤ p.natDegree
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<VAR>p : Polynomial R<GOAL>Multiset.count a p.roots = Polynomial.rootMultiplicity a p
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<GOAL>a ∈ p.roots ↔ p.IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>h : a ∈ p.roots<GOAL>p ≠ 0
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>h : a ∈ p.roots<GOAL>p.IsRoot a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>x : R<VAR>w : p ≠ 0<GOAL>x ∈ p.roots ↔ (Polynomial.aeval x) p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>Z : Finset R<VAR>h : Z.val ⊆ p.roots<GOAL>Z.card ≤ p.natDegree
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<GOAL>{x | p.IsRoot x}.Finite
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>h : {x | p.IsRoot x}.Infinite<GOAL>p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>LinearOrder R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<GOAL>∃ x₀, ∀ (x : R), p.IsRoot x → x ≤ x₀
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>LinearOrder R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<GOAL>∃ x₀, ∀ (x : R), p.IsRoot x → x₀ ≤ x
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : Polynomial R<VAR>h : {x | Polynomial.eval x p = Polynomial.eval x q}.Infinite<GOAL>p = q
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : Polynomial R<VAR>hpq : p * q ≠ 0<GOAL>(p * q).roots = p.roots + q.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : Polynomial R<VAR>h : q ≠ 0<GOAL>p ∣ q → p.roots ≤ q.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>a x : R<GOAL>x ∈ (p - Polynomial.C a).roots ↔ p ≠ Polynomial.C a ∧ Polynomial.eval x p = a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>a x : R<VAR>hp0 : 0 < p.degree<GOAL>x ∈ (p - Polynomial.C a).roots ↔ Polynomial.eval x p = a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>r : R<GOAL>(Polynomial.X - Polynomial.C r).roots = {r}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.X.roots = {0}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>x : R<GOAL>(Polynomial.C x).roots = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.roots 1 = ∅
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * p).roots = p.roots
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>ha : a ≠ 0<GOAL>(a • p).roots = p.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>(-p).roots = p.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>L : List (Polynomial R)<GOAL>0 ∉ L → L.prod.roots = (↑L).bind Polynomial.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>m : Multiset (Polynomial R)<GOAL>0 ∉ m → m.prod.roots = m.bind Polynomial.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>ι : Type u_1<VAR>f : ι → Polynomial R<VAR>s : Finset ι<GOAL>s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => (f i).roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>(p ^ n).roots = n • p.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).roots = n • {0}
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>(Polynomial.C a * Polynomial.X ^ n).roots = n • {0}
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>IsDomain R<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>((Polynomial.monomial n) a).roots = n • {0}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>s : Finset R<GOAL>(∏ a ∈ s, (Polynomial.X - Polynomial.C a)).roots = s.val
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>s : Multiset R<GOAL>(Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.roots = s
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>Multiset.card (Polynomial.X ^ n - Polynomial.C a).roots ≤ n
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a x : R<GOAL>x ∈ Polynomial.nthRoots n a ↔ x ^ n = a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>r : R<GOAL>Polynomial.nthRoots 0 r = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<GOAL>Polynomial.nthRoots n 0 = Multiset.replicate n 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>a : R<GOAL>Multiset.card (Polynomial.nthRoots n a) ≤ n
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>r : R<GOAL>Polynomial.nthRoots 2 r = 0 ↔ ¬IsSquare r
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<GOAL>Polynomial.nthRootsFinset n R = (Polynomial.nthRoots n 1).toFinset
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>h : 0 < n<VAR>x : R<GOAL>x ∈ Polynomial.nthRootsFinset n R ↔ x ^ n = 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Polynomial.nthRootsFinset 0 R = ∅
<VAR>R : Type u<VAR>n : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>η₁ η₂ : R<VAR>hη₁ : η₁ ∈ Polynomial.nthRootsFinset n R<VAR>hη₂ : η₂ ∈ Polynomial.nthRootsFinset n R<GOAL>η₁ * η₂ ∈ Polynomial.nthRootsFinset n R
<VAR>R : Type u<VAR>n : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>η : R<VAR>hη : η ∈ Polynomial.nthRootsFinset n R<GOAL>η ≠ 0
<VAR>R : Type u<VAR>n : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>hn : 0 < n<GOAL>1 ∈ Polynomial.nthRootsFinset n R
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>p : Polynomial R<VAR>h : ∀ (x : R), Polynomial.eval x p = 0<GOAL>p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>p q : Polynomial R<VAR>ext : ∀ (r : R), Polynomial.eval r p = Polynomial.eval r q<GOAL>p = q
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>p.aroots S = (Polynomial.map (algebraMap T S) p).roots
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>p : Polynomial T<VAR>a : S<GOAL>a ∈ p.aroots S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>p : Polynomial T<VAR>a : S<GOAL>a ∈ p.aroots S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>p q : Polynomial T<VAR>hpq : p * q ≠ 0<GOAL>(p * q).aroots S = p.aroots S + q.aroots S
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>r : T<GOAL>(Polynomial.X - Polynomial.C r).aroots S = {(algebraMap T S) r}
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>Polynomial.X.aroots S = {0}
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>a : T<GOAL>(Polynomial.C a).aroots S = 0
<VAR>T : Type w<VAR>CommRing T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>Polynomial.aroots 0 S = 0
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>Polynomial.aroots 1 S = 0
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>p : Polynomial T<GOAL>(-p).aroots S = p.aroots S
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>a : T<VAR>p : Polynomial T<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * p).aroots S = p.aroots S
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>a : T<VAR>p : Polynomial T<VAR>ha : a ≠ 0<GOAL>(a • p).aroots S = p.aroots S
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>p : Polynomial T<VAR>n : ℕ<GOAL>(p ^ n).aroots S = n • p.aroots S
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).aroots S = n • {0}
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>a : T<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>(Polynomial.C a * Polynomial.X ^ n).aroots S = n • {0}
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>a : T<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>((Polynomial.monomial n) a).aroots S = n • {0}
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>DecidableEq S<GOAL>p.rootSet S = ↑(p.aroots S).toFinset
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>a : T<GOAL>(Polynomial.C a).rootSet S = ∅
<VAR>T : Type w<VAR>CommRing T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>Polynomial.rootSet 0 S = ∅
<VAR>T : Type w<VAR>CommRing T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>Polynomial.rootSet 1 S = ∅
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>(-p).rootSet S = p.rootSet S
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<GOAL>(p.rootSet S).Finite
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>CommRing S<VAR>IsDomain S<VAR>DecidableEq S<VAR>m : R →+* S<VAR>d : ℕ<VAR>U : Set R<VAR>h : U.Finite<GOAL>(⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>a : S<GOAL>a ∈ p.rootSet S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>a : S<GOAL>a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>NoZeroSMulDivisors T S<VAR>hp : p ≠ 0<VAR>a : S<GOAL>a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>CommRing S'<VAR>IsDomain S'<VAR>Algebra T S'<VAR>hp : Polynomial.map (algebraMap T S') p = 0 → Polynomial.map (algebraMap T S) p = 0<VAR>f : S →ₐ[T] S'<GOAL>Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>a : S<VAR>h : a ∈ p.rootSet S<GOAL>p ≠ 0
<VAR>S : Type v<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>a : S<VAR>hx : a ∈ p.rootSet S<GOAL>(Polynomial.aeval a) p = 0
<VAR>T : Type w<VAR>CommRing T<VAR>p : Polynomial T<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra T S<VAR>CommRing S'<VAR>IsDomain S'<VAR>Algebra T S'<VAR>NoZeroSMulDivisors T S'<VAR>f : S →ₐ[T] S'<GOAL>Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>ι : Type u_2<VAR>Fintype ι<VAR>f : ι → R<VAR>hf : Function.Injective f<VAR>heval : ∀ (i : ι), Polynomial.eval (f i) p = 0<VAR>hcard : p.natDegree < Fintype.card ι<GOAL>p = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>s : Finset R<VAR>heval : ∀ i ∈ s, Polynomial.eval i p = 0<VAR>hcard : p.natDegree < s.card<GOAL>p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>f : Polynomial R<VAR>hf : ∀ (r : R), Polynomial.eval r f = 0<VAR>hfR : ↑f.natDegree < Cardinal.mk R<GOAL>f = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>f : Polynomial R<VAR>hf : f ≠ 0<VAR>hfR : ↑f.natDegree < Cardinal.mk R<GOAL>∃ r, Polynomial.eval r f ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>(Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod.Monic
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>DecidableEq R<GOAL>(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
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>(Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod ∣ p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<VAR>s : Multiset R<GOAL>(Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod ∣ p ↔ s ≤ p.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<GOAL>∃ q, (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod * q = p ∧ Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>hp : p.Monic<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>(Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>a p : Polynomial R<VAR>hp : p.Monic<VAR>hap : a ∣ p<GOAL>IsUnit a.leadingCoeff
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : Polynomial R<VAR>p_monic : p.Monic<VAR>p_1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (q : Polynomial R), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hmap : Polynomial.map f p ≠ 0<VAR>a : A<GOAL>Polynomial.rootMultiplicity a p ≤ Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>a : A<GOAL>Polynomial.rootMultiplicity a p = Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>DecidableEq B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hmap : Polynomial.map f p ≠ 0<VAR>b : B<GOAL>Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>DecidableEq B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>b : B<GOAL>Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>IsDomain B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>h : Polynomial.map f p ≠ 0<GOAL>Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>IsDomain B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<GOAL>Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>IsDomain B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>h : Polynomial.map f p ≠ 0<GOAL>Multiset.card p.roots ≤ Multiset.card (Polynomial.map f p).roots
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>IsDomain B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<GOAL>Multiset.card p.roots ≤ Multiset.card (Polynomial.map f p).roots
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain A<VAR>IsDomain B<VAR>p : Polynomial A<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : b ≤ c<VAR>a0 : 0 ≤ a<GOAL>a * b ≤ a * c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : b ≤ c<VAR>a0 : 0 ≤ a<GOAL>b * a ≤ c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>bc : b < c<VAR>a0 : 0 < a<GOAL>a * b < a * c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>bc : b < c<VAR>a0 : 0 < a<GOAL>b * a < c * a
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulReflectLT α<VAR>h : a * b < a * c<VAR>a0 : 0 ≤ a<GOAL>b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosReflectLT α<VAR>h : b * a < c * a<VAR>a0 : 0 ≤ a<GOAL>b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulReflectLE α<VAR>bc : a * b ≤ a * c<VAR>a0 : 0 < a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosReflectLE α<VAR>bc : b * a ≤ c * a<VAR>a0 : 0 < a<GOAL>b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>PosMulReflectLT α<VAR>a0 : 0 < a<GOAL>a * b < a * c ↔ b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>MulPosReflectLT α<VAR>a0 : 0 < a<GOAL>b * a < c * a ↔ b < c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>α : Type u_1<VAR>a b c : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>MulPosReflectLE α<VAR>a0 : 0 < a<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<VAR>a0 : 0 ≤ a<VAR>d0 : 0 ≤ d<GOAL>a * c ≤ b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<VAR>c0 : 0 ≤ c<VAR>b0 : 0 ≤ b<GOAL>a * c ≤ b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<VAR>a0 : 0 < a<VAR>d0 : 0 ≤ d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<VAR>c0 : 0 ≤ c<VAR>b0 : 0 < b<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<VAR>a0 : 0 ≤ a<VAR>d0 : 0 < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>MulPosStrictMono α<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<VAR>c0 : 0 < c<VAR>b0 : 0 ≤ b<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>h₁ : a < b<VAR>h₂ : c < d<VAR>a0 : 0 < a<VAR>d0 : 0 < d<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>h₁ : a < b<VAR>h₂ : c < d<VAR>c0 : 0 < c<VAR>b0 : 0 < b<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a * b ≤ c<VAR>hle : d ≤ b<VAR>a0 : 0 ≤ a<GOAL>a * d ≤ c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a * b < c<VAR>hle : d ≤ b<VAR>a0 : 0 ≤ a<GOAL>a * d < c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a ≤ b * c<VAR>hle : c ≤ d<VAR>b0 : 0 ≤ b<GOAL>a ≤ b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>PosMulMono α<VAR>h : a < b * c<VAR>hle : c ≤ d<VAR>b0 : 0 ≤ b<GOAL>a < b * d
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a * b ≤ c<VAR>hle : d ≤ a<VAR>b0 : 0 ≤ b<GOAL>d * b ≤ c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a * b < c<VAR>hle : d ≤ a<VAR>b0 : 0 ≤ b<GOAL>d * b < c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a ≤ b * c<VAR>hle : b ≤ d<VAR>c0 : 0 ≤ c<GOAL>a ≤ d * c
<VAR>α : Type u_1<VAR>a b c d : α<VAR>Mul α<VAR>Zero α<VAR>Preorder α<VAR>MulPosMono α<VAR>h : a < b * c<VAR>hle : b ≤ d<VAR>c0 : 0 ≤ c<GOAL>a < d * c
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>PosMulReflectLE α<GOAL>PosMulStrictMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>MulPosReflectLE α<GOAL>MulPosStrictMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<GOAL>PosMulStrictMono α ↔ PosMulReflectLE α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<GOAL>MulPosStrictMono α ↔ MulPosReflectLE α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>PosMulReflectLT α<GOAL>PosMulMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>MulPosReflectLT α<GOAL>MulPosMono α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>PosMulMono α<GOAL>PosMulReflectLT α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<VAR>MulPosMono α<GOAL>MulPosReflectLT α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<GOAL>PosMulMono α ↔ PosMulReflectLT α
<VAR>α : Type u_1<VAR>Mul α<VAR>Zero α<VAR>LinearOrder α<GOAL>MulPosMono α ↔ MulPosReflectLT α
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a * b < 0
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>PosMulStrictMono α<VAR>PosMulReflectLT α<VAR>h : 0 < a<GOAL>0 < a * b ↔ 0 < b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>α : Type u_1<VAR>a b : α<VAR>MulZeroClass α<VAR>Preorder α<VAR>MulPosStrictMono α<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a * b < 0