ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R[X]<GOAL>∀ (a : PolynomialModule R M), (PolynomialModule.comp p) a = (PolynomialModule.eval p) ((PolynomialModule.map R[X] (PolynomialModule.lsingle R 0)) a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R[X]<VAR>i : ℕ<VAR>m : M<GOAL>(PolynomialModule.comp p) ((PolynomialModule.single R i) m) = p ^ i • (PolynomialModule.single R 0) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(PolynomialModule.eval r) ((PolynomialModule.comp p) q) = (PolynomialModule.eval (Polynomial.eval r p)) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : R[X]<VAR>q : PolynomialModule R M<GOAL>(PolynomialModule.comp p) (p' • q) = p'.comp p • (PolynomialModule.comp p) q
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = p.degree
<VAR>R : Type u<VAR>Semiring R<GOAL>WellFounded fun p q => p.degree < q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>Subsingleton R<VAR>p : R[X]<GOAL>p.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.Monic ↔ p.leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p.leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p.coeff p.natDegree = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.degree 0 = ⊥
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.natDegree 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.coeff p.natDegree = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.degree = ⊥ ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.degree ≠ ⊥ ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>Subsingleton R<GOAL>p.degree = ⊥
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>Subsingleton R<GOAL>p.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>p.degree = ↑p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>p.degree = ↑n ↔ p.natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>p.degree = ↑n ↔ p.natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.degree = ↑n<GOAL>p.natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>p.natDegree ≠ n → p.degree ≠ ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.degree ≤ ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>q : S[X]<VAR>h : p.degree = q.degree<GOAL>p.natDegree = q.natDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>↑n ≤ p.degree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>n ≤ p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : ℕ<GOAL>a ∈ p.support → a ≤ p.natDegree
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>pn : p.degree ≤ ↑n<VAR>p1 : p.coeff n ≠ 0<GOAL>p.degree = ↑n
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>pn : p.natDegree ≤ n<VAR>p1 : p.coeff n ≠ 0<GOAL>p.natDegree = n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>f : R[X]<VAR>g : S[X]<VAR>h : f.support ⊆ g.support<GOAL>f.degree ≤ g.degree
<VAR>R : Type u<VAR>m : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.natDegree < m<GOAL>p.support ⊆ Finset.range m
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.support ⊆ Finset.range (p.natDegree + 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : q.coeff p.natDegree ≠ 0<GOAL>p.degree ≤ q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>p.natDegree ≤ n ↔ p.degree ≤ ↑n
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>p.natDegree < n ↔ p.degree < ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>p : R[X]<VAR>Semiring S<VAR>q : S[X]<VAR>hpq : p.degree ≤ q.degree<GOAL>p.natDegree ≤ q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hpq : p.degree < q.degree<GOAL>p.natDegree < q.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a).degree = 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>(Polynomial.C a).degree ≤ 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<GOAL>(Polynomial.C a).degree < 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.degree 1 ≤ 0
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).natDegree = 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.natDegree 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(↑n).natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(↑n).degree ≤ 0
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>((Polynomial.monomial n) a).degree = ↑n
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ n).degree = ↑n
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X).degree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>((Polynomial.monomial n) a).degree ≤ ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>(Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a * Polynomial.X).degree ≤ 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ n).natDegree = n
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X).natDegree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>DecidableEq R<VAR>i : ℕ<VAR>r : R<GOAL>((Polynomial.monomial i) r).natDegree = if r = 0 then 0 else i
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>m : ℕ<GOAL>((Polynomial.monomial m) a).natDegree ≤ m
<VAR>R : Type u<VAR>Semiring R<VAR>i : ℕ<VAR>r : R<VAR>r0 : r ≠ 0<GOAL>((Polynomial.monomial i) r).natDegree = i
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.degree < ↑n<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<GOAL>p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p.degree ≤ ↑n<VAR>hq : q.degree ≤ ↑n<GOAL>p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.coeff (p.natDegree + 1) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>I : Decidable (n < 1 + p.natDegree)<GOAL>(if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f : ℕ → R → S<VAR>h : ∀ (n : ℕ), f n 0 = 0<VAR>n : ℕ<VAR>w : p.natDegree < n<GOAL>p.sum f = ∑ a ∈ Finset.range n, f a (p.coeff a)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>AddCommMonoid S<VAR>p : R[X]<VAR>f : ℕ → R → S<VAR>h : ∀ (n : ℕ), f n 0 = 0<GOAL>p.sum f = ∑ a ∈ Finset.range (p.natDegree + 1), f a (p.coeff a)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>AddCommMonoid S<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>n : ℕ<VAR>p : R[X]<VAR>hn : p.degree < ↑n<GOAL>∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>w : p.natDegree < n<GOAL>p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff i)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hn : p.degree = ↑n<GOAL>p.coeff n ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.degree ≤ 1<GOAL>p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.degree = 1<GOAL>p = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.natDegree ≤ 1<GOAL>p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 1<GOAL>p = Polynomial.X + Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.natDegree ≤ 1<GOAL>∃ a b, p = Polynomial.C a * Polynomial.X + Polynomial.C b
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).degree ≤ ↑n
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.degree ≤ 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.natDegree ≤ 1
<VAR>R : Type u<VAR>Semiring R<VAR>n a : ℕ<VAR>c : R<VAR>h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support<GOAL>a = n
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<VAR>n : ℕ<GOAL>(Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.support.card ≤ p.natDegree + 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : ℕ<GOAL>a ∈ p.support → ↑a ≤ p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.degree 1 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.X.degree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<GOAL>Polynomial.X.natDegree = 1
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<VAR>r : R<VAR>a : ℕ<GOAL>(p * (Polynomial.X - Polynomial.C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).degree = p.degree
<VAR>R : Type u<VAR>Ring R<VAR>a : WithBot ℕ<VAR>p : R[X]<VAR>hp : p.degree ≤ a<GOAL>(-p).degree ≤ a
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).natDegree = p.natDegree
<VAR>R : Type u<VAR>m : ℕ<VAR>Ring R<VAR>p : R[X]<VAR>hp : p.natDegree ≤ m<GOAL>(-p).natDegree ≤ m
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<GOAL>(↑n).natDegree = 0
<VAR>R : Type u<VAR>Ring R<VAR>n : ℤ<GOAL>(↑n).degree ≤ 0
<VAR>R : Type u<VAR>Ring R<VAR>p : R[X]<GOAL>(-p).leadingCoeff = -p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>c : R<GOAL>(Polynomial.C c).nextCoeff = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>p.nextCoeff = p.coeff (p.natDegree - 1)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>p.coeff q.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : WithBot ℕ<VAR>h : n < p.degree<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hpq : p.degree ≤ q.degree<VAR>hp : p ≠ 0<GOAL>q ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : n < p.natDegree<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.natDegree < q.natDegree<GOAL>p.degree < q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p ≠ 0<GOAL>p.natDegree < q.natDegree ↔ p.degree < q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.degree ≤ 0<GOAL>p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.degree = 0<GOAL>p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.degree ≤ 0 ↔ p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p + q).degree ≤ max p.degree q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p.degree ≤ ↑n<VAR>hq : q.degree ≤ ↑n<GOAL>(p + q).degree ≤ ↑n
<VAR>R : Type u<VAR>Semiring 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>Semiring R<VAR>p q : R[X]<GOAL>(p + q).natDegree ≤ max p.natDegree q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ n<VAR>hq : q.natDegree ≤ n<GOAL>(p + q).natDegree ≤ n
<VAR>R : Type u<VAR>n m : ℕ<VAR>Semiring 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>Semiring R<GOAL>Polynomial.leadingCoeff 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.leadingCoeff = 0 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.leadingCoeff ≠ 0 ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.leadingCoeff = 0 ↔ p.degree = ⊥
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hf : p.natDegree ≤ n<VAR>hn : p.coeff n = 0<GOAL>p.natDegree ≤ n - 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>H : p ≠ 0<GOAL>p.natDegree ∈ p.support
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p ≠ 0<GOAL>p.natDegree = p.support.max' ⋯
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>(Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p + q).degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p + q).degree = q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : q.natDegree < p.natDegree<GOAL>(p + q).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.natDegree < q.natDegree<GOAL>(p + q).natDegree = q.natDegree
<VAR>R : Type u<VAR>a : R<VAR>Semiring R<VAR>p : R[X]<VAR>hp : 0 < p.degree<GOAL>(p + Polynomial.C a).degree = p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : R<GOAL>(p + Polynomial.C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : R<GOAL>(Polynomial.C a + p).natDegree = p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.leadingCoeff + q.leadingCoeff ≠ 0<GOAL>(p + q).degree = max p.degree q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>H : (p + q).natDegree < p.natDegree<GOAL>p.natDegree = q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>H : (p + q).natDegree < q.natDegree<GOAL>p.natDegree = q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>H : (p + q).natDegree = 0<GOAL>p.natDegree = q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(Polynomial.erase n p).degree ≤ p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>(Polynomial.erase p.natDegree p).degree < p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(p.update n a).degree ≤ max p.degree ↑n
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → R[X]<GOAL>(∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).degree ≤ p.degree + q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>a b : WithBot ℕ<VAR>hp : p.degree ≤ a<VAR>hq : q.degree ≤ b<GOAL>(p * q).degree ≤ a + b
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).degree ≤ n • p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>a : WithBot ℕ<VAR>b : ℕ<VAR>hp : p.degree ≤ a<GOAL>(p ^ b).degree ≤ ↑b * a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>((Polynomial.monomial n) a).leadingCoeff = a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>(Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a * Polynomial.X).leadingCoeff = a
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.C a).leadingCoeff = a
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.leadingCoeff = 1
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).Monic
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.X.Monic
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.leadingCoeff 1 = 1
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.Monic 1
<VAR>R : Type u_2<VAR>Semiring R<VAR>Nontrivial R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>h : 0 ≠ 1<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>pn : p.natDegree ≤ n<VAR>p1 : p.coeff n = 1<GOAL>p.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>pn : p.degree ≤ ↑n<VAR>p1 : p.coeff n = 1<GOAL>p.Monic
<VAR>R : Type u<VAR>Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hne : q ≠ r<GOAL>p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p + q).leadingCoeff = q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : q.degree < p.degree<GOAL>(p + q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.degree = q.degree<VAR>hlc : p.leadingCoeff + q.leadingCoeff ≠ 0<GOAL>(p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).degree = p.degree + q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>(p * q).degree = p.degree + q.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.support.card ≤ 1<GOAL>(Polynomial.monomial p.natDegree) p.leadingCoeff = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.support.card ≤ 1<GOAL>Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<GOAL>p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>p.leadingCoeff ^ n ≠ 0 → (p ^ n).degree = n • p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<GOAL>(p ^ n).natDegree = n * p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.Monic<GOAL>(p * q).leadingCoeff = q.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>(p * q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p * Polynomial.X ^ n).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>(p * Polynomial.X).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>Semiring R<VAR>p q : R[X]<GOAL>(p * q).natDegree ≤ p.natDegree + q.natDegree
<VAR>R : Type u<VAR>n m : ℕ<VAR>Semiring R<VAR>p q : R[X]<VAR>hp : p.natDegree ≤ m<VAR>hg : q.natDegree ≤ n<GOAL>(p * q).natDegree ≤ m + n
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).natDegree ≤ n * p.natDegree
<VAR>R : Type u<VAR>m : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>hp : p.natDegree ≤ m<GOAL>(p ^ n).natDegree ≤ n * m
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
<VAR>R : Type u<VAR>Semiring R<VAR>df dg : ℕ<VAR>f g : R[X]<VAR>hdf : f.natDegree ≤ df<VAR>hdg : g.natDegree ≤ dg<GOAL>(f * g).coeff (df + dg) = f.coeff df * g.coeff dg
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>0 ≤ p.degree ↔ p ≠ 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natDegree = 0 ↔ p.degree ≤ 0
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.degree 0 ≤ 0
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>n : WithBot ℕ<GOAL>f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>p : R[X]<GOAL>(a • p).degree ≤ p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>a : R<VAR>p : R[X]<GOAL>(a • p).natDegree ≤ p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hp : p ≠ 0<GOAL>p.degree < (p * Polynomial.X).degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>0 < p.natDegree ↔ 0 < p.degree
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.natDegree ≤ 0<GOAL>p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>h : p.natDegree = 0<GOAL>p = Polynomial.C (p.coeff 0)
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p.natDegree = 0 ↔ ∃ x, Polynomial.C x = p
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<GOAL>p = Polynomial.C (p.coeff 0) ↔ p.natDegree = 0
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hf : p.Monic<VAR>hfd : p.natDegree = 0<GOAL>p = 1
<VAR>R : Type u<VAR>Semiring R<VAR>p : R[X]<VAR>hf : p.Monic<GOAL>p.natDegree = 0 ↔ p = 1
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hdeg : ↑n ≤ p.degree<GOAL>p ≠ 0
<VAR>R : Type u<VAR>n : ℕ<VAR>Semiring R<VAR>p : R[X]<VAR>hdeg : ↑n ≤ p.degree<GOAL>n ≤ p.natDegree
<VAR>R : Type u<VAR>Semiring R<VAR>n : ℕ<VAR>f : Fin n → R<GOAL>(∑ i : Fin n, Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C b).degree < (Polynomial.C a * Polynomial.X).degree
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).degree = 1
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree = 1
<VAR>R : Type u<VAR>a b : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X + Polynomial.C b).leadingCoeff = a
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C b * Polynomial.X + Polynomial.C c).degree < (Polynomial.C a * Polynomial.X ^ 2).degree
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree ≤ 2
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree = 2
<VAR>R : Type u<VAR>a b c : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).leadingCoeff = a
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < 4
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < (Polynomial.C a * Polynomial.X ^ 3).degree
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree = 3
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree ≤ 3
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree = 3
<VAR>R : Type u<VAR>a b c d : R<VAR>Semiring R<VAR>ha : a ≠ 0<GOAL>(Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).leadingCoeff = a
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).degree = ↑n