ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>Semiring S<VAR>Nontrivial S<VAR>p : R[X]<VAR>f : R →+* S<GOAL>(Polynomial.map f p).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>p : R[X]<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<GOAL>(Polynomial.map f p).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>p : R[X]<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<GOAL>(Polynomial.map f p).leadingCoeff = f p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(Polynomial.map f p).Monic ↔ p.Monic
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<GOAL>IsUnit p ↔ p.degree = 0
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<GOAL>q * p.div q + p.mod q = p
<VAR>R : Type u<VAR>Field R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : q ≠ 0<GOAL>(p.mod q).degree < q.degree
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<GOAL>p / q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<GOAL>p % q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
<VAR>R : Type u<VAR>Field R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : q.Monic<GOAL>p %ₘ q = p % q
<VAR>R : Type u<VAR>Field R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : q.Monic<GOAL>p /ₘ q = p / q
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>a : R<GOAL>p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
<VAR>R : Type u<VAR>a : R<VAR>Field R<VAR>p : R[X]<GOAL>(Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<GOAL>p % q = p ↔ p.degree < q.degree
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<GOAL>p / q = 0 ↔ p.degree < q.degree
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<VAR>hq0 : q ≠ 0<VAR>hpq : q.degree ≤ p.degree<GOAL>q.degree + (p / q).degree = p.degree
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<GOAL>(p / q).degree ≤ p.degree
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : 0 < q.degree<GOAL>(p / q).degree < p.degree
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p : R[X]<VAR>Field k<VAR>f : R →+* k<GOAL>IsUnit (Polynomial.map f p) ↔ IsUnit p
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p q : R[X]<VAR>Field k<VAR>f : R →+* k<GOAL>Polynomial.map f (p / q) = Polynomial.map f p / Polynomial.map f q
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p q : R[X]<VAR>Field k<VAR>f : R →+* k<GOAL>Polynomial.map f (p % q) = Polynomial.map f p % Polynomial.map f q
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p q : R[X]<VAR>Field k<VAR>DecidableEq R<VAR>DecidableEq k<VAR>f : R →+* k<GOAL>EuclideanDomain.gcd (Polynomial.map f p) (Polynomial.map f q) = Polynomial.map f (EuclideanDomain.gcd p q)
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>CommSemiring k<VAR>DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hf : Polynomial.eval₂ ϕ α f = 0<VAR>hg : Polynomial.eval₂ ϕ α g = 0<GOAL>Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
<VAR>R : Type u<VAR>Field R<VAR>DecidableEq R<VAR>f g : R[X]<VAR>α : R<VAR>hf : Polynomial.eval α f = 0<VAR>hg : Polynomial.eval α g = 0<GOAL>Polynomial.eval α (EuclideanDomain.gcd f g) = 0
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>CommSemiring k<VAR>DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<GOAL>Polynomial.eval₂ ϕ α f = 0
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>CommSemiring k<VAR>DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<GOAL>Polynomial.eval₂ ϕ α g = 0
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>CommSemiring k<VAR>DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<GOAL>Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 ↔ Polynomial.eval₂ ϕ α f = 0 ∧ Polynomial.eval₂ ϕ α g = 0
<VAR>R : Type u<VAR>Field R<VAR>DecidableEq R<VAR>f g : R[X]<VAR>α : R<GOAL>(EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p q : R[X]<VAR>Field k<VAR>f : R →+* k<GOAL>IsCoprime (Polynomial.map f p) (Polynomial.map f q) ↔ IsCoprime p q
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>p : R[X]<VAR>CommRing k<VAR>IsDomain k<VAR>f : R →+* k<VAR>x : k<VAR>hp : p ≠ 0<GOAL>x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Field R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : R<VAR>ha : a ≠ 0<GOAL>((Polynomial.monomial n) a).rootSet S = {0}
<VAR>R : Type u<VAR>S : Type v<VAR>Field R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ n).rootSet S = {0}
<VAR>R : Type u<VAR>S : Type v<VAR>Field R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(Polynomial.X ^ n).rootSet S = {0}
<VAR>R : Type u<VAR>S : Type v<VAR>Field R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s : Finset ι<VAR>h : s.prod f ≠ 0<GOAL>(s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>h : p.degree = 1<GOAL>∃ x, p.IsRoot x
<VAR>R : Type u<VAR>Field R<VAR>u : R[X]ˣ<VAR>n : ℕ<GOAL>((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>DecidableEq R<VAR>hp0 : p ≠ 0<GOAL>(normalize p).Monic
<VAR>R : Type u<VAR>Field R<VAR>p q : R[X]<VAR>hpq : q.degree ≤ p.degree<GOAL>(p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
<VAR>R : Type u<VAR>a : R<VAR>Field R<VAR>p q : R[X]<GOAL>p / (Polynomial.C a * q) = Polynomial.C a⁻¹ * (p / q)
<VAR>R : Type u<VAR>a : R<VAR>Field R<VAR>p q : R[X]<VAR>ha : a ≠ 0<GOAL>Polynomial.C a * p ∣ q ↔ p ∣ q
<VAR>R : Type u<VAR>a : R<VAR>Field R<VAR>p q : R[X]<VAR>ha : a ≠ 0<GOAL>p ∣ Polynomial.C a * q ↔ p ∣ q
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>DecidableEq R<VAR>hp : p ≠ 0<GOAL>↑(normUnit p) = Polynomial.C p.leadingCoeff⁻¹
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>DecidableEq R<VAR>h : p.Monic<GOAL>normalize p = p
<VAR>R : Type u<VAR>k : Type y<VAR>Field R<VAR>Field k<VAR>f : R →+* k<VAR>x y : R[X]<GOAL>Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>DecidableEq R<GOAL>(normalize p).degree = p.degree
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>hp1 : p.degree = 1<GOAL>Prime p
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>hp1 : p.degree = 1<GOAL>Irreducible p
<VAR>R : Type u<VAR>Field R<VAR>x : R<GOAL>¬Irreducible (Polynomial.C x)
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>hp : Irreducible p<GOAL>0 < p.degree
<VAR>K : Type u_1<VAR>Field K<VAR>f : K[X]<VAR>a : K<GOAL>(Polynomial.X - Polynomial.C a) * (f /ₘ (Polynomial.X - Polynomial.C a)) = f - f %ₘ (Polynomial.X - Polynomial.C a)
<VAR>K : Type u_1<VAR>Field K<VAR>f : K[X]<VAR>a : K<GOAL>f /ₘ (Polynomial.X - Polynomial.C a) + (Polynomial.X - Polynomial.C a) * Polynomial.derivative (f /ₘ (Polynomial.X - Polynomial.C a)) = Polynomial.derivative f
<VAR>K : Type u_1<VAR>Field K<VAR>f : K[X]<VAR>a : K<VAR>hf : Polynomial.X - Polynomial.C a ∣ f /ₘ (Polynomial.X - Polynomial.C a)<GOAL>Polynomial.X - Polynomial.C a ∣ Polynomial.derivative f
<VAR>K : Type u_1<VAR>Field K<VAR>f : K[X]<VAR>a : K<VAR>hf' : Polynomial.eval a (Polynomial.derivative f) ≠ 0<GOAL>IsCoprime (Polynomial.X - Polynomial.C a) (f /ₘ (Polynomial.X - Polynomial.C a))
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>R : Type u<VAR>Field R<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>F : Type u_1<VAR>Field F<VAR>f : F[X]<VAR>h : Irreducible f<GOAL>0 < f.natDegree
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>q : ℚ≥0<GOAL>0 ≤ ↑q
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>q : ℚ≥0<VAR>ha : 0 ≤ a<GOAL>0 ≤ q • a
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : { x // 0 ≤ x }<GOAL>↑a⁻¹ = (↑a)⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>x : α<VAR>hx : 0 ≤ x<GOAL>⟨x, hx⟩⁻¹ = ⟨x⁻¹, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a b : { x // 0 ≤ x }<GOAL>↑(a / b) = ↑a / ↑b
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>x y : α<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>⟨x, hx⟩ / ⟨y, hy⟩ = ⟨x / y, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : { x // 0 ≤ x }<VAR>n : ℤ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>n : ℤ<GOAL>⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>q : ℚ≥0<GOAL>⟨↑q, ⋯⟩ = ↑q
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>q : ℚ≥0<VAR>a : { x // 0 ≤ x }<GOAL>↑(q • a) = q • ↑a
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>q : ℚ≥0<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⟨q • a, ⋯⟩ = q • a
<VAR>α : Type u_1<VAR>Sub α<VAR>Bot α<VAR>a b : α<GOAL>↑(a - b) = ↑a - ↑b
<VAR>α : Type u_1<VAR>Sub α<VAR>Bot α<VAR>a : α<GOAL>⊤ - ↑a = ⊤
<VAR>α : Type u_1<VAR>Sub α<VAR>Bot α<VAR>a : WithTop α<GOAL>a - ⊤ = ↑⊥
<VAR>α : Type u_1<VAR>Sub α<VAR>Bot α<VAR>a b : WithTop α<GOAL>a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Sub α<VAR>Bot α<VAR>Sub β<VAR>Bot β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x - y) = f x - f y<VAR>h₀ : f ⊥ = ⊥<VAR>x y : WithTop α<GOAL>WithTop.map f (x - y) = WithTop.map f x - WithTop.map f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>a : α<VAR>s : Set β<VAR>ha : 0 ≤ a<GOAL>a • lowerBounds s ⊆ lowerBounds (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>a : α<VAR>s : Set β<VAR>ha : 0 ≤ a<GOAL>a • upperBounds s ⊆ upperBounds (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>a : α<VAR>s : Set β<VAR>hs : BddBelow s<VAR>ha : 0 ≤ a<GOAL>BddBelow (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>a : α<VAR>s : Set β<VAR>hs : BddAbove s<VAR>ha : 0 ≤ a<GOAL>BddAbove (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>GroupWithZero α<VAR>Zero β<VAR>MulActionWithZero α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>s : Set β<VAR>a : α<VAR>ha : 0 < a<GOAL>lowerBounds (a • s) = a • lowerBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>GroupWithZero α<VAR>Zero β<VAR>MulActionWithZero α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>s : Set β<VAR>a : α<VAR>ha : 0 < a<GOAL>upperBounds (a • s) = a • upperBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>GroupWithZero α<VAR>Zero β<VAR>MulActionWithZero α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>s : Set β<VAR>a : α<VAR>ha : 0 < a<GOAL>BddBelow (a • s) ↔ BddBelow s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>GroupWithZero α<VAR>Zero β<VAR>MulActionWithZero α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>s : Set β<VAR>a : α<VAR>ha : 0 < a<GOAL>BddAbove (a • s) ↔ BddAbove s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a ≤ 0<GOAL>a • lowerBounds s ⊆ upperBounds (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a ≤ 0<GOAL>a • upperBounds s ⊆ lowerBounds (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a ≤ 0<VAR>hs : BddBelow s<GOAL>BddAbove (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a ≤ 0<VAR>hs : BddAbove s<GOAL>BddBelow (a • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a < 0<GOAL>lowerBounds (a • s) = a • upperBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a < 0<GOAL>upperBounds (a • s) = a • lowerBounds s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a < 0<GOAL>BddBelow (a • s) ↔ BddAbove s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>OrderedAddCommGroup β<VAR>Module α β<VAR>PosSMulMono α β<VAR>s : Set β<VAR>a : α<VAR>ha : a < 0<GOAL>BddAbove (a • s) ↔ BddBelow s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>OrderedSemiring R<VAR>OrderedAddCommMonoid M<VAR>SMulWithZero R M<VAR>self : OrderedSMul R M<VAR>a b : M<VAR>c : R<GOAL>a < b → 0 < c → c • a < c • b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>OrderedSemiring R<VAR>OrderedAddCommMonoid M<VAR>SMulWithZero R M<VAR>self : OrderedSMul R M<VAR>a b : M<VAR>c : R<GOAL>c • a < c • b → 0 < c → a < b
<VAR>𝕜 : Type u_5<VAR>M : Type u_7<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid M<VAR>SMulWithZero 𝕜 M<VAR>h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a => c • a<GOAL>OrderedSMul 𝕜 M
<VAR>𝕜 : Type u_5<VAR>M : Type u_7<VAR>LinearOrderedSemifield 𝕜<VAR>OrderedAddCommMonoid M<VAR>MulActionWithZero 𝕜 M<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<GOAL>OrderedSMul 𝕜 M
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>Semiring α<VAR>Invertible 2<VAR>Lattice β<VAR>AddCommGroup β<VAR>Module α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊓ y = ⅟2 • (x + y - |y - x|)
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>Semiring α<VAR>Invertible 2<VAR>Lattice β<VAR>AddCommGroup β<VAR>Module α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊔ y = ⅟2 • (x + y + |y - x|)
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>DivisionSemiring α<VAR>NeZero 2<VAR>Lattice β<VAR>AddCommGroup β<VAR>Module α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊓ y = 2⁻¹ • (x + y - |y - x|)
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>DivisionSemiring α<VAR>NeZero 2<VAR>Lattice β<VAR>AddCommGroup β<VAR>Module α β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊔ y = 2⁻¹ • (x + y + |y - x|)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>OrderedSemiring β<VAR>Algebra α β<VAR>SMulPosMono α β<GOAL>Monotone ⇑(algebraMap α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>OrderedSemiring β<VAR>Algebra α β<VAR>SMulPosMono α β<VAR>a₁ a₂ : α<VAR>ha : a₁ ≤ a₂<GOAL>(algebraMap α β) a₁ ≤ (algebraMap α β) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>OrderedSemiring β<VAR>Algebra α β<VAR>SMulPosMono α β<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ (algebraMap α β) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>StrictOrderedSemiring β<VAR>Algebra α β<VAR>SMulPosMono α β<VAR>SMulPosReflectLE α β<VAR>a₁ a₂ : α<GOAL>(algebraMap α β) a₁ ≤ (algebraMap α β) a₂ ↔ a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>StrictOrderedSemiring β<VAR>Algebra α β<VAR>SMulPosStrictMono α β<GOAL>StrictMono ⇑(algebraMap α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>StrictOrderedSemiring β<VAR>Algebra α β<VAR>SMulPosStrictMono α β<VAR>a₁ a₂ : α<VAR>ha : a₁ < a₂<GOAL>(algebraMap α β) a₁ < (algebraMap α β) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>StrictOrderedSemiring β<VAR>Algebra α β<VAR>SMulPosStrictMono α β<VAR>a : α<VAR>ha : 0 < a<GOAL>0 < (algebraMap α β) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedCommSemiring α<VAR>StrictOrderedSemiring β<VAR>Algebra α β<VAR>SMulPosStrictMono α β<VAR>a₁ a₂ : α<VAR>SMulPosReflectLT α β<GOAL>(algebraMap α β) a₁ < (algebraMap α β) a₂ ↔ a₁ < a₂
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<GOAL>Polynomial.X ∣ f ↔ f.coeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>Polynomial.X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : 0 < p.degree<VAR>hmp : p.Monic<VAR>hq : q ≠ 0<GOAL>multiplicity.Finite p q
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>hq : q.Monic<GOAL>(p - q * (Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree))).degree < p.degree
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>q : R[X]<VAR>_hq : q.Monic<GOAL>(p %ₘ q).degree < q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>hmq : q.Monic<VAR>hq : q ≠ 1<GOAL>(p %ₘ q).natDegree < q.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>0 %ₘ p = 0
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>0 /ₘ p = 0
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p %ₘ 0 = p
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p /ₘ 0 = 0
<VAR>R : Type u<VAR>Ring R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : ¬q.Monic<GOAL>p /ₘ q = 0
<VAR>R : Type u<VAR>Ring R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : ¬q.Monic<GOAL>p %ₘ q = p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>Nontrivial R<VAR>hq : q.Monic<GOAL>p %ₘ q = p ↔ p.degree < q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>hq : q.Monic<GOAL>(p %ₘ q).degree ≤ q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>(p %ₘ g).natDegree ≤ g.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>Polynomial.X ∣ p - Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>_hq : q.Monic<GOAL>p %ₘ q = p - q * (p /ₘ q)
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>hq : q.Monic<GOAL>p %ₘ q + q * (p /ₘ q) = p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>Nontrivial R<VAR>hq : q.Monic<GOAL>p /ₘ q = 0 ↔ p.degree < q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<GOAL>q.degree + (p /ₘ q).degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<GOAL>(p /ₘ q).degree ≤ p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<GOAL>(p /ₘ q).degree < p.degree
<VAR>R : Type u<VAR>Ring R<VAR>f : R[X]<VAR>g : R[X]<VAR>hg : g.Monic<GOAL>(f /ₘ g).natDegree = f.natDegree - g.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>f g : R[X]<VAR>q r : R[X]<VAR>hg : g.Monic<VAR>h : r + g * q = f ∧ r.degree < g.degree<GOAL>f /ₘ g = q ∧ f %ₘ g = r
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>p q : R[X]<VAR>Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<GOAL>Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q ∧ Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>p q : R[X]<VAR>Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<GOAL>Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>p q : R[X]<VAR>Ring S<VAR>f : R →+* S<VAR>hq : q.Monic<GOAL>Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>p %ₘ q = 0 ↔ q ∣ p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>q * p %ₘ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R[X]<VAR>hx : x.Monic<GOAL>Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p %ₘ 1 = 0
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>p /ₘ 1 = p
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>n : ℕ<VAR>hn : q.degree ≤ ↑n<GOAL>∑ i : Fin n, (Polynomial.monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>q : R[X]<VAR>hmo : q.Monic<GOAL>q * p /ₘ q = p
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<GOAL>(p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (Polynomial.X - Polynomial.C a)).coeff (n + 1)
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<GOAL>(p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = ∑ i ∈ Finset.Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<VAR>h0 : p ≠ 0<GOAL>multiplicity.Finite (Polynomial.X - Polynomial.C a) p
<VAR>R : Type u<VAR>Ring R<VAR>DecidableEq R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<GOAL>Polynomial.rootMultiplicity a p = Nat.find ⋯
<VAR>R : Type u<VAR>Ring R<VAR>DecidableEq R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p : R[X]<VAR>a : R<GOAL>Polynomial.rootMultiplicity a p = if h0 : p = 0 then 0 else (multiplicity (Polynomial.X - Polynomial.C a) p).get ⋯
<VAR>R : Type u<VAR>Ring R<VAR>x : R<GOAL>Polynomial.rootMultiplicity x 0 = 0
<VAR>R : Type u<VAR>Ring R<VAR>r a : R<GOAL>Polynomial.rootMultiplicity a (Polynomial.C r) = 0
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<GOAL>(Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p ∣ p
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<GOAL>(Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) = p
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>a : R<GOAL>∃ q, p = (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * q ∧ ¬Polynomial.X - Polynomial.C a ∣ q
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>a : R<GOAL>p %ₘ (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>p : R[X]<GOAL>(Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>p : R[X]<GOAL>Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>p : R[X]<GOAL>Polynomial.X - Polynomial.C a ∣ p - Polynomial.C (Polynomial.eval a p)
<VAR>R : Type u<VAR>a : R<VAR>CommRing R<VAR>b : R[X]<VAR>P : R[X][X]<GOAL>P ∈ Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} ↔ Polynomial.eval a (Polynomial.eval b P) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<GOAL>p %ₘ Polynomial.X = Polynomial.C (Polynomial.eval 0 p)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>x : S<VAR>hx : Polynomial.eval₂ f x q = 0<GOAL>Polynomial.eval₂ f x (p %ₘ q) = Polynomial.eval₂ f x p
<VAR>R : Type u<VAR>CommRing R<VAR>a b : R<VAR>p : R[X]<GOAL>a - b ∣ Polynomial.eval a p - Polynomial.eval b p
<VAR>R : Type u<VAR>CommRing R<VAR>x : R<GOAL>RingHom.ker (Polynomial.evalRingHom x) = Ideal.span {Polynomial.X - Polynomial.C x}
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>x : R<GOAL>Polynomial.rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>x : R<VAR>h : ¬p.IsRoot x<GOAL>Polynomial.rootMultiplicity x p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>x : R<GOAL>0 < Polynomial.rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>x : R<GOAL>0 < Polynomial.rootMultiplicity x p ↔ p.IsRoot x
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>a : R<VAR>hp : p ≠ 0<GOAL>Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>p * q %ₘ q = 0
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>Preorder α<VAR>a b : AddUnits α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>Preorder α<VAR>a b : αˣ<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>Preorder α<VAR>a b : AddUnits α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>Monoid α<VAR>Preorder α<VAR>a b : αˣ<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>LinearOrder α<GOAL>⇑AddUnits.orderEmbeddingVal = AddUnits.val
<VAR>α : Type u_1<VAR>Monoid α<VAR>LinearOrder α<GOAL>⇑Units.orderEmbeddingVal = Units.val
<VAR>α : Type u_1<VAR>Monoid α<VAR>LinearOrder α<VAR>a b : αˣ<GOAL>↑(max a b) = max ↑a ↑b
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>LinearOrder α<VAR>a b : AddUnits α<GOAL>↑(max a b) = max ↑a ↑b
<VAR>α : Type u_1<VAR>Monoid α<VAR>LinearOrder α<VAR>a b : αˣ<GOAL>↑(min a b) = min ↑a ↑b
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>LinearOrder α<VAR>a b : AddUnits α<GOAL>↑(min a b) = min ↑a ↑b