ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>(p * Polynomial.X).natDegree = p.natDegree + 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>(Polynomial.X * p).natDegree = p.natDegree + 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(p * Polynomial.X ^ n).natDegree = p.natDegree + n
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(Polynomial.X ^ n * p).natDegree = p.natDegree + n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).natDegree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>¬IsUnit Polynomial.X
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<GOAL>(p * Polynomial.X).degree = p.degree + 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p * Polynomial.X ^ n).degree = p.degree + ↑n
<VAR>R : Type u<VAR>a : R<VAR>Ring R<VAR>p : R[X]<VAR>hp : 0 < p.degree<GOAL>(p - Polynomial.C a).degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>a : R<GOAL>(p - Polynomial.C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<GOAL>(p - q).degree ≤ max p.degree q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>a b : WithBot ℕ<VAR>hp : p.degree ≤ a<VAR>hq : q.degree ≤ b<GOAL>(p - q).degree ≤ max a b
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p - q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p - q).leadingCoeff = -q.leadingCoeff
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : p.degree = q.degree<VAR>hlc : p.leadingCoeff ≠ q.leadingCoeff<GOAL>(p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<GOAL>(p - q).natDegree ≤ max p.natDegree q.natDegree
<VAR>R : Type u<VAR>n m : ℕ<VAR>Ring R<VAR>p q : R[X]<VAR>hp : p.natDegree ≤ m<VAR>hq : q.natDegree ≤ n<GOAL>(p - q).natDegree ≤ max m n
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>hd : p.degree = q.degree<VAR>hp0 : p ≠ 0<VAR>hlc : p.leadingCoeff = q.leadingCoeff<GOAL>(p - q).degree < p.degree
<VAR>R : Type u<VAR>Ring R<VAR>r : R<GOAL>(Polynomial.X - Polynomial.C r).degree ≤ 1
<VAR>R : Type u<VAR>Ring R<VAR>r : R<GOAL>(Polynomial.X - Polynomial.C r).natDegree ≤ 1
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p - q).degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p - q).degree = q.degree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : q.natDegree < p.natDegree<GOAL>(p - q).natDegree = p.natDegree
<VAR>R : Type u<VAR>Ring R<VAR>p q : R[X]<VAR>h : p.natDegree < q.natDegree<GOAL>(p - q).natDegree = q.natDegree
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.X + Polynomial.C a).degree = 1
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>x : R<GOAL>(Polynomial.X + Polynomial.C x).natDegree = 1
<VAR>S : Type v<VAR>Semiring S<VAR>c : S<GOAL>(Polynomial.X + Polynomial.C c).nextCoeff = c
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>(Polynomial.X ^ n + Polynomial.C a).degree = ↑n
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>Polynomial.X ^ n + Polynomial.C a ≠ 0
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.X + Polynomial.C r ≠ 0
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>α : Type u_1<VAR>m : Multiset α<VAR>f : α → R<GOAL>0 ∉ Multiset.map (fun a => Polynomial.X + Polynomial.C (f a)) m
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>(Polynomial.X ^ n + Polynomial.C r).natDegree = n
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>Polynomial.X ^ n + Polynomial.C a ≠ 1
<VAR>R : Type u<VAR>Nontrivial R<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.X + Polynomial.C r ≠ 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>r : R<GOAL>(Polynomial.X ^ n + Polynomial.C r).leadingCoeff = 1
<VAR>S : Type v<VAR>Semiring S<VAR>r : S<GOAL>(Polynomial.X + Polynomial.C r).leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(Polynomial.X ^ n + 1).leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>r : R<VAR>i : ℕ<GOAL>((Polynomial.X + Polynomial.C r) ^ i).leadingCoeff = 1
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>r : R<GOAL>(Polynomial.X ^ n - Polynomial.C r).leadingCoeff = 1
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(Polynomial.X ^ n - 1).leadingCoeff = 1
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>a : R<GOAL>(Polynomial.X - Polynomial.C a).degree = 1
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>x : R<GOAL>(Polynomial.X - Polynomial.C x).natDegree = 1
<VAR>S : Type v<VAR>Ring S<VAR>c : S<GOAL>(Polynomial.X - Polynomial.C c).nextCoeff = -c
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>(Polynomial.X ^ n - Polynomial.C a).degree = ↑n
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>Polynomial.X ^ n - Polynomial.C a ≠ 0
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>r : R<GOAL>Polynomial.X - Polynomial.C r ≠ 0
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>α : Type u_1<VAR>m : Multiset α<VAR>f : α → R<GOAL>0 ∉ Multiset.map (fun a => Polynomial.X - Polynomial.C (f a)) m
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>n : ℕ<VAR>r : R<GOAL>(Polynomial.X ^ n - Polynomial.C r).natDegree = n
<VAR>S : Type v<VAR>Ring S<VAR>r : S<GOAL>(Polynomial.X - Polynomial.C r).leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).degree = p.degree + q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).degree = n • p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<GOAL>Polynomial.leadingCoeffHom p = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).leadingCoeff = p.leadingCoeff ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>a p : R[X]<VAR>hap : a ∣ p<GOAL>a.leadingCoeff ∣ p.leadingCoeff
<VAR>N i : ℕ<GOAL>Polynomial.revAtFun N (Polynomial.revAtFun N i) = i
<VAR>N : ℕ<GOAL>Function.Injective (Polynomial.revAtFun N)
<VAR>N i : ℕ<GOAL>Polynomial.revAtFun N i = (Polynomial.revAt N) i
<VAR>N i : ℕ<GOAL>(Polynomial.revAt N) ((Polynomial.revAt N) i) = i
<VAR>N i : ℕ<VAR>H : i ≤ N<GOAL>(Polynomial.revAt N) i = N - i
<VAR>N i : ℕ<VAR>h : N < i<GOAL>(Polynomial.revAt N) i = i
<VAR>N O n o : ℕ<VAR>hn : n ≤ N<VAR>ho : o ≤ O<GOAL>(Polynomial.revAt (N + O)) (n + o) = (Polynomial.revAt N) n + (Polynomial.revAt O) o
<VAR>N : ℕ<GOAL>(Polynomial.revAt N) 0 = N
<VAR>R : Type u_1<VAR>Semiring R<VAR>N : ℕ<VAR>f : Polynomial R<GOAL>(Polynomial.reflect N f).support = Finset.image (⇑(Polynomial.revAt N)) f.support
<VAR>R : Type u_1<VAR>Semiring R<VAR>N : ℕ<VAR>f : Polynomial R<VAR>i : ℕ<GOAL>(Polynomial.reflect N f).coeff i = f.coeff ((Polynomial.revAt N) i)
<VAR>R : Type u_1<VAR>Semiring R<VAR>N : ℕ<GOAL>Polynomial.reflect N 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>N : ℕ<VAR>f : Polynomial R<GOAL>Polynomial.reflect N f = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : Polynomial R<VAR>N : ℕ<GOAL>Polynomial.reflect N (f + g) = Polynomial.reflect N f + Polynomial.reflect N g
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<VAR>r : R<VAR>N : ℕ<GOAL>Polynomial.reflect N (Polynomial.C r * f) = Polynomial.C r * Polynomial.reflect N f
<VAR>R : Type u_1<VAR>Semiring R<VAR>N n : ℕ<VAR>c : R<GOAL>Polynomial.reflect N (Polynomial.C c * Polynomial.X ^ n) = Polynomial.C c * Polynomial.X ^ (Polynomial.revAt N) n
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>N : ℕ<GOAL>Polynomial.reflect N (Polynomial.C r) = Polynomial.C r * Polynomial.X ^ N
<VAR>R : Type u_1<VAR>Semiring R<VAR>N n : ℕ<GOAL>Polynomial.reflect N (Polynomial.X ^ n) = Polynomial.X ^ (Polynomial.revAt N) n
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.reflect 1 Polynomial.X = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>cf cg N O : ℕ<VAR>f g : Polynomial R<GOAL>f.support.card ≤ cf.succ → g.support.card ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → Polynomial.reflect (N + O) (f * g) = Polynomial.reflect N f * Polynomial.reflect O g
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : Polynomial R<VAR>F G : ℕ<VAR>Ff : f.natDegree ≤ F<VAR>Gg : g.natDegree ≤ G<GOAL>Polynomial.reflect (F + G) (f * g) = Polynomial.reflect F f * Polynomial.reflect G g
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>Invertible x<VAR>N : ℕ<VAR>f : Polynomial R<VAR>hf : f.natDegree ≤ N<GOAL>Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) * x ^ N = Polynomial.eval₂ i x f
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>Invertible x<VAR>N : ℕ<VAR>f : Polynomial R<VAR>hf : f.natDegree ≤ N<GOAL>Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) = 0 ↔ Polynomial.eval₂ i x f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<VAR>n : ℕ<GOAL>f.reverse.coeff n = f.coeff ((Polynomial.revAt f.natDegree) n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.coeff 0 = f.leadingCoeff
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.reverse 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.natDegree ≤ f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.natDegree = f.reverse.natDegree + f.natTrailingDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.natDegree = f.natDegree - f.natTrailingDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.leadingCoeff = f.trailingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.natTrailingDegree = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.trailingCoeff = f.leadingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : Polynomial R<VAR>fg : f.leadingCoeff * g.leadingCoeff ≠ 0<GOAL>(f * g).reverse = f.reverse * g.reverse
<VAR>R : Type u_2<VAR>Ring R<VAR>NoZeroDivisors R<VAR>f g : Polynomial R<GOAL>(f * g).reverse = f.reverse * g.reverse
<VAR>R : Type u_2<VAR>Ring R<VAR>NoZeroDivisors R<VAR>p q : Polynomial R<GOAL>(p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Polynomial R<GOAL>f.reverse.coeff 1 = f.nextCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>t : R<GOAL>(Polynomial.C t).reverse = Polynomial.C t
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>(p * Polynomial.X).reverse = p.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>(Polynomial.X * p).reverse = p.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>(p * Polynomial.X ^ n).reverse = p.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n * p).reverse = p.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>t : R<GOAL>(p + Polynomial.C t).reverse = p.reverse + Polynomial.C t * Polynomial.X ^ p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>t : R<GOAL>(Polynomial.C t + p).reverse = Polynomial.C t * Polynomial.X ^ p.natDegree + p.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>Invertible x<VAR>f : Polynomial R<GOAL>Polynomial.eval₂ i (⅟x) f.reverse * x ^ f.natDegree = Polynomial.eval₂ i x f
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>Invertible x<VAR>f : Polynomial R<GOAL>Polynomial.eval₂ i (⅟x) f.reverse = 0 ↔ Polynomial.eval₂ i x f = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>f : Polynomial R<VAR>N : ℕ<GOAL>Polynomial.reflect N (-f) = -Polynomial.reflect N f
<VAR>R : Type u_1<VAR>Ring R<VAR>f g : Polynomial R<VAR>N : ℕ<GOAL>Polynomial.reflect N (f - g) = Polynomial.reflect N f - Polynomial.reflect N g
<VAR>R : Type u_1<VAR>Ring R<VAR>f : Polynomial R<GOAL>(-f).reverse = -f.reverse
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<GOAL>Polynomial.trinomial k m n u v w = Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(Polynomial.trinomial k m n u v w).coeff n = w
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(Polynomial.trinomial k m n u v w).coeff m = v
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(Polynomial.trinomial k m n u v w).coeff k = u
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).natDegree = n
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).natTrailingDegree = k
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hw : w ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).leadingCoeff = w
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).trailingCoeff = u
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(Polynomial.trinomial k m n u v 1).Monic
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>hw : w ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).mirror = Polynomial.trinomial k (n - m + k) n w v u
<VAR>R : Type u_1<VAR>Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<GOAL>(Polynomial.trinomial k m n u v w).support = {k, m, n}
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<GOAL>¬IsUnit p
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<GOAL>p.support.card = 3
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<GOAL>p ≠ 0
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<VAR>k : ℕ<VAR>hk : k ∈ p.support<GOAL>IsUnit (p.coeff k)
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<GOAL>IsUnit p.leadingCoeff
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<GOAL>IsUnit p.trailingCoeff
<VAR>p : Polynomial ℤ<GOAL>p.IsUnitTrinomial ↔ p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
<VAR>p : Polynomial ℤ<GOAL>p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3
<VAR>p q : Polynomial ℤ<VAR>h : p * p.mirror = q * q.mirror<GOAL>p.IsUnitTrinomial ↔ q.IsUnitTrinomial
<VAR>p : Polynomial ℤ<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w<GOAL>Polynomial.C ↑v * (Polynomial.C ↑u * Polynomial.X ^ (m + n) + Polynomial.C ↑w * Polynomial.X ^ (n - m + k + n)) = { toFinsupp := Finsupp.filter (fun x => x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }
<VAR>p q : Polynomial ℤ<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w : ℤˣ<VAR>hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w<VAR>hq : q = Polynomial.trinomial k m' n ↑u ↑v ↑w<VAR>h : p * p.mirror = q * q.mirror<GOAL>q = p ∨ q = p.mirror
<VAR>p q : Polynomial ℤ<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w<VAR>hq : q = Polynomial.trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<GOAL>q = p ∨ q = p.mirror
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<VAR>h : IsRelPrime p p.mirror<GOAL>Irreducible p
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<VAR>h : IsCoprime p p.mirror<GOAL>Irreducible p
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.support = f.support.erase f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<GOAL>f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.coeff f.natDegree = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : i ≠ f.natDegree<GOAL>f.eraseLead.coeff i = f.coeff i
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.eraseLead 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead + (Polynomial.monomial f.natDegree) f.leadingCoeff = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead + Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f
<VAR>R : Type u_2<VAR>Ring R<VAR>f : R[X]<GOAL>f - (Polynomial.monomial f.natDegree) f.leadingCoeff = f.eraseLead
<VAR>R : Type u_2<VAR>Ring R<VAR>f : R[X]<GOAL>f - Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f.eraseLead
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>f0 : 2 ≤ f.support.card<GOAL>f.eraseLead ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>a : ℕ<VAR>h : a ∈ f.eraseLead.support<GOAL>a < f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>a : ℕ<VAR>h : a ∈ f.eraseLead.support<GOAL>a ≠ f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.natDegree ∉ f.eraseLead.support
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<GOAL>f.eraseLead.support.card < f.support.card
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<GOAL>f.eraseLead.support.card + 1 = f.support.card
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.support.card = f.support.card - 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>c : ℕ<VAR>fc : f.support.card = c + 1<GOAL>f.eraseLead.support.card = c
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h₀ : f ≠ 0<VAR>h₁ : f.eraseLead = 0<GOAL>f.support.card = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead = 0<GOAL>f.support.card ≤ 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>i : ℕ<VAR>r : R<GOAL>((Polynomial.monomial i) r).eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>(Polynomial.C r).eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Polynomial.X.eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(Polynomial.C r * Polynomial.X ^ n).eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>(Polynomial.C r * Polynomial.X).eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : R[X]<VAR>pq : q.natDegree < p.natDegree<GOAL>(p + q).eraseLead = p.eraseLead + q
<VAR>R : Type u_1<VAR>Semiring R<VAR>p q : R[X]<VAR>pq : p.natDegree < q.natDegree<GOAL>(p + q).eraseLead = p + q.eraseLead
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.degree ≤ f.degree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.natDegree ≤ f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>f0 : 2 ≤ f.support.card<GOAL>f.eraseLead.natDegree < f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead ≠ 0<GOAL>0 < f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.natDegree = f.natDegree - 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.natDegree + 1 = f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff = 0<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 2
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>hlead : f.eraseLead ≠ 0<VAR>hnext : f.nextCoeff = 0<GOAL>2 ≤ f.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.leadingCoeff = f.nextCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead = 0<GOAL>f.nextCoeff = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>P : R[X] → Prop<VAR>N : ℕ<VAR>P_0 : P 0<VAR>P_C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → P (Polynomial.C r * Polynomial.X ^ n)<VAR>P_C_add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → P f → P g → P (f + g)<VAR>f : R[X]<GOAL>f.natDegree ≤ N → P f
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Semiring S<VAR>FunLike F R[X] S[X]<VAR>AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>k : ℕ<VAR>fu : ℕ → ℕ<VAR>fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0<VAR>fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m<VAR>φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0<VAR>φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = fu n<GOAL>(φ p).natDegree = fu p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Semiring S<VAR>FunLike F R[X] S[X]<VAR>AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>k : ℕ<VAR>φ_k : ∀ (f : R[X]), f.natDegree < k → φ f = 0<VAR>φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n - k<GOAL>(φ p).natDegree = p.natDegree - k
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>F : Type u_3<VAR>Semiring S<VAR>FunLike F R[X] S[X]<VAR>AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n<GOAL>(φ p).natDegree = p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>k : Fin n → ℕ<VAR>x : Fin n → R<VAR>hk : Function.Injective k<VAR>hx : ∀ (i : Fin n), x i ≠ 0<GOAL>(∑ i : Fin n, Polynomial.C (x i) * Polynomial.X ^ k i).support.card = n
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.support.card = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, Polynomial.C (x i) * Polynomial.X ^ k i
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.support.card = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = Polynomial.C x * Polynomial.X ^ k
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.support.card = 2 ↔ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : R[X]<GOAL>f.support.card = 3 ↔ ∃ k m n, ∃ (_ : k < m) (_ : m < n), ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n
<VAR>K : Type u_1<VAR>LinearOrderedRing K<VAR>FloorRing K<VAR>n : ℕ<VAR>a c : K<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p < ↑(p - 1).factorial
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>n : ℕ<VAR>a c : K<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p / ↑(p - 1).factorial < 1
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>FloorSemiring α<VAR>a : { r // 0 ≤ r }<GOAL>⌊↑a⌋₊ = ⌊a⌋₊
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>FloorSemiring α<VAR>a : { r // 0 ≤ r }<GOAL>⌈↑a⌉₊ = ⌈a⌉₊
<VAR>α : Type u<VAR>self : IdemSemiring α<VAR>a : α<GOAL>IdemSemiring.bot ≤ a
<VAR>α : Type u<VAR>self : IdemSemiring α<VAR>a b : α<GOAL>a + b = a ⊔ b
<VAR>α : Type u_5<VAR>self : KleeneAlgebra α<VAR>a b : α<GOAL>b * a ≤ b → b * a∗ ≤ b
<VAR>α : Type u_5<VAR>self : KleeneAlgebra α<VAR>a b : α<GOAL>a * b ≤ b → a∗ * b ≤ b
<VAR>α : Type u_5<VAR>self : KleeneAlgebra α<VAR>a : α<GOAL>a * a∗ ≤ a∗
<VAR>α : Type u_5<VAR>self : KleeneAlgebra α<VAR>a : α<GOAL>a∗ * a ≤ a∗
<VAR>α : Type u_5<VAR>self : KleeneAlgebra α<VAR>a : α<GOAL>1 ≤ a∗
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a b : α<GOAL>a + b = a ⊔ b
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a : α<GOAL>a + a = a
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>n : ℕ<GOAL>n ≠ 0 → ∀ (a : α), n • a = a
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a b : α<GOAL>a + b = a ↔ b ≤ a
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a b : α<GOAL>a + b = b ↔ a ≤ b
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a b c : α<GOAL>a + b ≤ c ↔ a ≤ c ∧ b ≤ c
<VAR>α : Type u_1<VAR>IdemSemiring α<VAR>a b c : α<VAR>ha : a ≤ c<VAR>hb : b ≤ c<GOAL>a + b ≤ c
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>1 ≤ a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a * a∗ ≤ a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a : α<GOAL>a∗ * a ≤ a∗
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b : α<GOAL>b * a ≤ b → b * a∗ ≤ b
<VAR>α : Type u_1<VAR>KleeneAlgebra α<VAR>a b : α<GOAL>a * b ≤ b → a∗ * b ≤ b