ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>m n : α<GOAL>(OrderEmbedding.addLeft m) n = m + n
<VAR>α : Type u_2<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>m n : α<GOAL>(OrderEmbedding.mulLeft m) n = m * n
<VAR>α : Type u_2<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>m n : α<GOAL>(OrderEmbedding.addRight m) n = n + m
<VAR>α : Type u_2<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>m n : α<GOAL>(OrderEmbedding.mulRight m) n = n * m
<VAR>α : Type u_3<VAR>LE α<VAR>Add α<VAR>Sub α<VAR>self : OrderedSub α<VAR>a b c : α<GOAL>a - b ≤ c ↔ a ≤ c + b
<VAR>α : Type u_1<VAR>LE α<VAR>Add α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - b ≤ c ↔ a ≤ c + b
<VAR>α : Type u_1<VAR>Preorder α<VAR>Add α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a + b - b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Add α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>b ≤ b - a + a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - b ≤ c ↔ a ≤ b + c
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a ≤ b + (a - b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a + b - a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>h : a ≤ b<VAR>c : α<GOAL>a - c ≤ b - c
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - b ≤ c ↔ a - c ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>b - (b - a) ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ b<VAR>c : α<GOAL>c - b ≤ c - a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a - d ≤ b - c
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>Antitone fun x => c - x
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - c ≤ a + (b - c)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - c ≤ a - c + b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b ≤ a + c + (b - c)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b ≤ a - c + (b + c)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a - c ≤ a - b + (b - c)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>c - a - (c - b) ≤ b - a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a - (b - c) ≤ a - b + c
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - (c + d) ≤ a - c + (b - d)
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - (a + c) ≤ b - c
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + c - (b + c) ≤ a - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>hb : AddLECancellable b<GOAL>a ≤ b + a - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>hb : AddLECancellable b<GOAL>a ≤ a + b - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>h : a + b ≤ c<GOAL>b ≤ c - a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : a + b ≤ c<GOAL>a ≤ c - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a ≤ b + a - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a ≤ a + b - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a + b ≤ c<GOAL>b ≤ c - a
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a + b ≤ c<GOAL>a ≤ c - b
<VAR>α : Type u_1<VAR>Preorder α<VAR>AddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b ≤ 0 ↔ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>b a c : α<GOAL>b - a - c = b - (a + c)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - (b + c) = a - b - c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - (b + c) = a - c - b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<GOAL>a - b - c = a - c - b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : a = c + b<GOAL>a - b = c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : a + c = b<GOAL>a = b - c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : a = b + c<GOAL>a - b = c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>hb : AddLECancellable b<GOAL>a + b - b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ha : AddLECancellable a<GOAL>a + b - a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : a - b < c<GOAL>a < b + c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : a - c < b<GOAL>a < b + c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : a + c < b<GOAL>a < b - c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>h : a + c < b<GOAL>c < b - a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a = c + b<GOAL>a - b = c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a + c = b<GOAL>a = b - c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a = b + c<GOAL>a - b = c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a + b - b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a + b - a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a - b < c<GOAL>a < b + c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a - c < b<GOAL>a < b + c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + c < b → c < b - a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + c < b → a < b - c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>a + c - (b + c) = a - b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a + b - (a + c) = b - c
<VAR>α : Type u_1<VAR>a b c : α<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>h : a - c < b - c<GOAL>a < b
<VAR>α : Type u_1<VAR>a b c : α<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<GOAL>a < b - c ↔ a + c < b
<VAR>α : Type u_1<VAR>a b c : α<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<GOAL>a < b - c ↔ c + a < b
<VAR>α : Type u_1<VAR>a b c : α<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<GOAL>a < b - c ↔ c < b - a
<VAR>α : Type u_1<VAR>a b c : α<VAR>LinearOrder α<VAR>AddCommSemigroup α<VAR>Sub α<VAR>OrderedSub α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a - b < a - c<GOAL>c < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>AddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a : α<GOAL>a - 0 = a
<VAR>α : Type u<VAR>Mul α<VAR>LE α<VAR>self : ExistsMulOfLE α<VAR>a b : α<GOAL>a ≤ b → ∃ c, b = a * c
<VAR>α : Type u<VAR>Add α<VAR>LE α<VAR>self : ExistsAddOfLE α<VAR>a b : α<GOAL>a ≤ b → ∃ c, b = a + c
<VAR>α : Type u<VAR>AddZeroClass α<VAR>Preorder α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ExistsAddOfLE α<VAR>a b : α<VAR>h : a < b<GOAL>∃ c, 0 < c ∧ a + c = b
<VAR>α : Type u<VAR>MulOneClass α<VAR>Preorder α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ExistsMulOfLE α<VAR>a b : α<VAR>h : a < b<GOAL>∃ c, 1 < c ∧ a * c = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>AddMonoid α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 0 < ε → a ≤ b + ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>Monoid α<VAR>ExistsMulOfLE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a ≤ b * ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>AddMonoid α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 0 < ε → a < b + ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>Monoid α<VAR>ExistsMulOfLE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a < b * ε<GOAL>a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>AddMonoid α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
<VAR>α : Type u<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>Monoid α<VAR>ExistsMulOfLE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>z : S<VAR>hz : (Polynomial.aeval z) p = 0<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<GOAL>0 < p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>Algebra R S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>z : S<VAR>hz : (Polynomial.aeval z) p = 0<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<GOAL>0 < p.degree
<VAR>R : Type u<VAR>CommRing R<VAR>q : R[X]<VAR>hq : q.Monic<VAR>p₁ p₂ : R[X]<VAR>h : q ∣ p₁ - p₂<GOAL>p₁ %ₘ q = p₂ %ₘ q
<VAR>R : Type u<VAR>CommRing R<VAR>q : R[X]<VAR>p₁ p₂ : R[X]<GOAL>(p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
<VAR>R : Type u<VAR>CommRing R<VAR>q : R[X]<VAR>c : R<VAR>p : R[X]<GOAL>c • p %ₘ q = c • (p %ₘ q)
<VAR>R : Type u<VAR>CommRing R<VAR>q p : R[X]<GOAL>q.modByMonicHom p = p %ₘ q
<VAR>R : Type u<VAR>CommRing R<VAR>p mod : R[X]<GOAL>-p %ₘ mod = -(p %ₘ mod)
<VAR>R : Type u<VAR>CommRing R<VAR>a b mod : R[X]<GOAL>(a - b) %ₘ mod = a %ₘ mod - b %ₘ mod
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>x : S<VAR>hx : (Polynomial.aeval x) q = 0<GOAL>(Polynomial.aeval x) (p %ₘ q) = (Polynomial.aeval x) p
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).trailingDegree = p.trailingDegree + q.trailingDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).natDegree = n * p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>q : R[X]<VAR>p : R[X]<VAR>hq : q ≠ 0<GOAL>p.degree ≤ (p * q).degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h1 : p ∣ q<VAR>h2 : q ≠ 0<GOAL>p.natDegree ≤ q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h1 : p ∣ q<VAR>h2 : q ≠ 0<GOAL>p.degree ≤ q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h₁ : p ∣ q<VAR>h₂ : q.degree < p.degree<GOAL>q = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h₁ : p ∣ q<VAR>h₂ : q.natDegree < p.natDegree<GOAL>q = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h0 : q ≠ 0<VAR>hl : q.degree < p.degree<GOAL>¬p ∣ q
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h0 : q ≠ 0<VAR>hl : q.natDegree < p.natDegree<GOAL>¬p ∣ q
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p₁ p₂ q₁ q₂ : R[X]<VAR>hp₁ : p₁ ≠ 0<VAR>hq₁ : q₁ ≠ 0<VAR>hp₂ : p₂ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h_eq : p₁ * q₂ = p₂ * q₁<GOAL>↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>h : IsUnit p<GOAL>p.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>Nontrivial R<VAR>h : IsUnit p<GOAL>p.degree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>u : R[X]ˣ<GOAL>(↑u).degree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<GOAL>IsUnit p ↔ ∃ r, IsUnit r ∧ Polynomial.C r = p
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hpl : 0 < p.degree<GOAL>¬IsUnit p
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hpl : 0 < p.natDegree<GOAL>¬IsUnit p
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Finset.Ioc 0 (p.natDegree / 2)
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<GOAL>¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
<VAR>R : Type u<VAR>a : R<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
<VAR>R : Type u<VAR>a : R<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<VAR>h : (p * q).IsRoot a<GOAL>p.IsRoot a ∨ q.IsRoot a
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>a : R<GOAL>Polynomial.C a ∣ p ↔ IsUnit a
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>0 < p.natDegree ↔ p ≠ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>0 < p.degree ↔ p ≠ 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hu : ¬IsUnit p<GOAL>0 < p.degree
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hu : ¬IsUnit p<GOAL>0 < p.natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>a p : R[X]<VAR>hp : p.Monic<VAR>ha : ¬IsUnit a<VAR>hap : a ∣ p<GOAL>0 < a.degree
<VAR>R : Type u<VAR>CommSemiring R<VAR>a p : R[X]<VAR>hp : p.Monic<VAR>ha : ¬IsUnit a<VAR>hap : a ∣ p<GOAL>0 < a.natDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>P : R[X]<VAR>h : ∀ (r : R), r • P = 0 → r = 0<VAR>Q : R[X]<GOAL>P * Q = 0 → Q = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>P : R[X]<GOAL>P ∉ nonZeroDivisors R[X] ↔ ∃ a, a ≠ 0 ∧ a • P = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>P : R[X]<GOAL>P ∈ nonZeroDivisors R[X] ↔ ∀ (a : R), a • P = 0 → a = 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<VAR>n : ℕ<GOAL>n ≤ Polynomial.rootMultiplicity a p ↔ (Polynomial.X - Polynomial.C a) ^ n ∣ p
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<VAR>n : ℕ<GOAL>Polynomial.rootMultiplicity a p ≤ n ↔ ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<GOAL>¬(Polynomial.X - Polynomial.C a) ^ (Polynomial.rootMultiplicity a p + 1) ∣ p
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<GOAL>(Polynomial.X - Polynomial.C t) ^ n ∣ p ↔ Polynomial.X ^ n ∣ p.comp (Polynomial.X + Polynomial.C t)
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>p.comp (Polynomial.X + Polynomial.C t) = 0 ↔ p = 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>p.comp (Polynomial.X + Polynomial.C t) ≠ 0 ↔ p ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>Polynomial.rootMultiplicity t p = Polynomial.rootMultiplicity 0 (p.comp (Polynomial.X + Polynomial.C t))
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<GOAL>Polynomial.rootMultiplicity 0 p = p.natTrailingDegree
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>Polynomial.rootMultiplicity t p = (p.comp (Polynomial.X + Polynomial.C t)).natTrailingDegree
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) = (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>h : p.Monic<GOAL>p ∈ nonZeroDivisors R[X]
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>h : p.leadingCoeff ∈ nonZeroDivisors R<GOAL>p ∈ nonZeroDivisors R[X]
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p ≠ 0<GOAL>Polynomial.rootMultiplicity a (p * (Polynomial.X - Polynomial.C a) ^ n) = Polynomial.rootMultiplicity a p + n
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>a : R<VAR>n : ℕ<GOAL>Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>x : R<GOAL>Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>DecidableEq R<VAR>x y : R<GOAL>Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C y) = if x = y then 1 else 0
<VAR>R : Type u<VAR>CommRing R<VAR>p q : R[X]<VAR>a : R<VAR>hzero : p + q ≠ 0<GOAL>min (Polynomial.rootMultiplicity a p) (Polynomial.rootMultiplicity a q) ≤ Polynomial.rootMultiplicity a (p + q)
<VAR>R : Type u<VAR>CommRing R<VAR>p q : R[X]<VAR>x : R<VAR>hpq : p * q ≠ 0<GOAL>Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q ≤ Polynomial.rootMultiplicity x (p * q)
<VAR>R : Type u<VAR>CommRing R<VAR>p q : R[X]<VAR>x : R<VAR>hpq : Polynomial.eval x (p /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x p) * Polynomial.eval x (q /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x q) ≠ 0<GOAL>Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>u : R[X]ˣ<GOAL>(↑u).natDegree = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>u : R[X]ˣ<GOAL>(↑u).coeff 0 ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<VAR>h : Associated p q<GOAL>p.degree = q.degree
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hi : Irreducible p<VAR>x : R<VAR>hx : p.IsRoot x<GOAL>p.degree = 1
<VAR>R : Type u<VAR>CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<GOAL>(p /ₘ q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<VAR>a : R<GOAL>(p /ₘ (Polynomial.X - Polynomial.C a)).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<VAR>hpq : p ∣ q<VAR>h₁ : q.natDegree ≤ p.natDegree<VAR>h₂ : p.leadingCoeff = q.leadingCoeff<GOAL>p = q
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<VAR>hpq : p ∣ q<VAR>h₁ : q.natDegree ≤ p.natDegree<VAR>h₂ : q.leadingCoeff ∣ p.leadingCoeff<GOAL>Associated p q
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hpq : p ∣ q<VAR>hq : q ≠ 0<VAR>h₁ : q.natDegree ≤ p.natDegree<GOAL>Associated p q
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hpq : p ∣ q<VAR>h₁ : p.degree = q.degree<GOAL>Associated p q
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hdiv : p ∣ q<VAR>hdeg : q.natDegree ≤ p.natDegree<GOAL>q = Polynomial.C q.leadingCoeff * p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>hdiv : p ∣ q<VAR>hdeg : q.natDegree ≤ p.natDegree<GOAL>q = p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>r : R<GOAL>Prime (Polynomial.X - Polynomial.C r)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Prime Polynomial.X
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hp1 : p.degree = 1<VAR>hm : p.Monic<GOAL>Prime p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>r : R<GOAL>Irreducible (Polynomial.X - Polynomial.C r)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>Irreducible Polynomial.X
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hp1 : p.degree = 1<VAR>hm : p.Monic<GOAL>Irreducible p
<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.natDegree = Multiset.card s