Loogle!

Result

Found 498 declarations mentioning Polynomial.degree. Of these, only the first 200 are shown.

• Polynomial.degree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) : WithBot ℕ
• Polynomial.degree_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.degree = 1
• Polynomial.degree_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.degree 0 = ⊥
• Polynomial.degree_X_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.degree ≤ 1
• Polynomial.degree_erase_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).degree ≤ p.degree
• Polynomial.degree_ne_of_natDegree_ne 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≠ n → p.degree ≠ ↑n
• Polynomial.natDegree_eq_of_degree_eq_some 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.degree = ↑n) : p.natDegree = n
• Polynomial.degree_le_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.degree ≤ ↑p.natDegree
• Polynomial.degree_neg 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (p : Polynomial R) : (-p).degree = p.degree
• Polynomial.natDegree_eq_of_degree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {q : Polynomial S} (h : p.degree = q.degree) : p.natDegree = q.natDegree
• Polynomial.degree_eq_iff_natDegree_eq_of_neZero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} [NeZero n] : p.degree = ↑n ↔ p.natDegree = n
• Polynomial.degree_le_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≤ n → p.degree ≤ ↑n
• Polynomial.degree_one 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.degree 1 = 0
• Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff = 0 ↔ p.degree = ⊥
• Polynomial.natDegree_le_of_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.degree ≤ ↑n → p.natDegree ≤ n
• Polynomial.degree_eq_bot 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.degree = ⊥ ↔ p = 0
• Polynomial.degree_natCast_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (↑n).degree ≤ 0
• Polynomial.degree_ne_bot 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.degree ≠ ⊥ ↔ p ≠ 0
• Polynomial.natDegree_le_iff_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.natDegree ≤ n ↔ p.degree ≤ ↑n
• Polynomial.coeff_ne_zero_of_eq_degree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hn : p.degree = ↑n) : p.coeff n ≠ 0
• Polynomial.degree_eq_iff_natDegree_eq_of_pos 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : 0 < n) : p.degree = ↑n ↔ p.natDegree = n
• Polynomial.degree_one_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.degree 1 ≤ 0
• Polynomial.degree_zero_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.degree 0 ≤ 0
• Polynomial.degree_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.degree = ↑p.natDegree
• Polynomial.degree_intCast_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (n : ℤ) : (↑n).degree ≤ 0
• Polynomial.natDegree_le_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {q : Polynomial S} (hpq : p.degree ≤ q.degree) : p.natDegree ≤ q.natDegree
• Polynomial.natDegree_eq_zero_iff_degree_le_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ p.degree ≤ 0
• Polynomial.le_degree_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : ↑n ≤ p.degree
• Polynomial.natDegree_pos_iff_degree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : 0 < p.natDegree ↔ 0 < p.degree
• Polynomial.degree_eq_iff_natDegree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p ≠ 0) : p.degree = ↑n ↔ p.natDegree = n
• Polynomial.degree_le_degree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.coeff p.natDegree ≠ 0) : p.degree ≤ q.degree
• Polynomial.degree_erase_lt 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : (Polynomial.erase p.natDegree p).degree < p.degree
• Polynomial.degree_mono 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : Polynomial R} {g : Polynomial S} (h : f.support ⊆ g.support) : f.degree ≤ g.degree
• Polynomial.degree_update_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p.update n a).degree ≤ max p.degree ↑n
• Polynomial.withBotSucc_degree_eq_natDegree_add_one 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.degree.succ = p.natDegree + 1
• Polynomial.degree_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (Polynomial.X ^ n).degree = ↑n
• Polynomial.degree_lt_iff_coeff_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (f : Polynomial R) (n : ℕ) : f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0
• Polynomial.degree_neg_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {a : WithBot ℕ} {p : Polynomial R} (hp : p.degree ≤ a) : (-p).degree ≤ a
• Polynomial.natDegree_lt_iff_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.natDegree < n ↔ p.degree < ↑n
• Polynomial.degree_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).degree ≤ ↑n
• Polynomial.degree_le_iff_coeff_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (f : Polynomial R) (n : WithBot ℕ) : f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
• Polynomial.degree_add_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p q : Polynomial R) : (p + q).degree ≤ max p.degree q.degree
• Polynomial.degree_mul_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).degree ≤ p.degree + q.degree
• Polynomial.degree_C_lt 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).degree < 1
• Polynomial.degree_C_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).degree ≤ 0
• Polynomial.degree_sum_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
• Polynomial.degree_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p ^ n).degree ≤ n • p.degree
• Polynomial.degree_C 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a).degree = 0
• Polynomial.degree_sub_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (p q : Polynomial R) : (p - q).degree ≤ max p.degree q.degree
• Polynomial.degree_C_mul_X_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).degree ≤ 1
• Polynomial.degree_add_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} {a b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p + q).degree ≤ max a b
• Polynomial.degree_mul_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} {a b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p * q).degree ≤ a + b
• Polynomial.degree_add_le_of_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.degree ≤ ↑n) (hq : q.degree ≤ ↑n) : (p + q).degree ≤ ↑n
• Polynomial.degree_C_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X).degree = 1
• Polynomial.degree_monomial_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).degree ≤ ↑n
• Polynomial.degree_sub_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} {a b : WithBot ℕ} (hp : p.degree ≤ a) (hq : q.degree ≤ b) : (p - q).degree ≤ max a b
• Polynomial.degree_pow_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {a : WithBot ℕ} (b : ℕ) (hp : p.degree ≤ a) : (p ^ b).degree ≤ ↑b * a
• Polynomial.degree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : ((Polynomial.monomial n) a).degree = ↑n
• Polynomial.degree_C_mul_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n
• Polynomial.degree_sub_lt 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < p.degree
• Polynomial.degree_sub_lt_left 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < p.degree
• Polynomial.degree_sub_lt_right 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hq0 : q ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < q.degree
• Polynomial.degree_X_sub_C_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (r : R) : (Polynomial.X - Polynomial.C r).degree ≤ 1
• Polynomial.degree_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).degree = ↑n
• Polynomial.degree_of_subsingleton 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} [Subsingleton R] : p.degree = ⊥
• Polynomial.degree_lt_wf 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] : WellFounded fun p q => p.degree < q.degree
• Polynomial.natDegree_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} {q : Polynomial S} (hpq : p.degree = q.degree) : p.natDegree = q.natDegree
• Polynomial.degree_lt_degree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.natDegree < q.natDegree) : p.degree < q.degree
• Polynomial.ne_zero_of_degree_gt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : WithBot ℕ} (h : n < p.degree) : p ≠ 0
• Polynomial.coeff_eq_zero_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.degree < ↑n) : p.coeff n = 0
• Polynomial.supDegree_eq_degree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] (p : Polynomial R) : AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = p.degree
• Polynomial.coeff_natDegree_eq_zero_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : p.coeff q.natDegree = 0
• Polynomial.monic_of_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.degree ≤ ↑n) (p1 : p.coeff n = 1) : p.Monic
• Polynomial.leadingCoeff_add_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).leadingCoeff = q.leadingCoeff
• Polynomial.leadingCoeff_add_of_degree_lt' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).leadingCoeff = p.leadingCoeff
• Polynomial.natDegree_add_eq_left_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).natDegree = p.natDegree
• Polynomial.natDegree_add_eq_right_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).natDegree = q.natDegree
• Polynomial.degree_add_eq_left_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).degree = p.degree
• Polynomial.degree_add_eq_right_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).degree = q.degree
• Polynomial.natDegree_lt_natDegree_iff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p ≠ 0) : p.natDegree < q.natDegree ↔ p.degree < q.degree
• Polynomial.natDegree_lt_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} {q : Polynomial S} (hp : p ≠ 0) (hpq : p.degree < q.degree) : p.natDegree < q.natDegree
• Polynomial.degree_eq_of_le_of_coeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.degree ≤ ↑n) (p1 : p.coeff n ≠ 0) : p.degree = ↑n
• Polynomial.Monic.degree_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) : (p * q).degree = p.degree + q.degree
• Polynomial.degree_lt_degree_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.degree < (p * Polynomial.X).degree
• Polynomial.degree_smul_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (p : Polynomial R) : (a • p).degree ≤ p.degree
• Polynomial.ne_zero_of_degree_ge_degree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0
• Polynomial.degree_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} : (p * Polynomial.X).degree = p.degree + 1
• Polynomial.degree_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : (p * q).degree = p.degree + q.degree
• Polynomial.Monic.degree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : 0 < p.degree ↔ p ≠ 1
• Polynomial.degree_le_mul_left 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R) (hq : q ≠ 0) : p.degree ≤ (p * q).degree
• Polynomial.leadingCoeff_sub_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p - q).leadingCoeff = p.leadingCoeff
• Polynomial.degree_sub_eq_left_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p - q).degree = p.degree
• Polynomial.degree_sub_eq_right_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p - q).degree = q.degree
• Polynomial.ext_iff_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.degree ≤ ↑n) (hq : q.degree ≤ ↑n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
• Polynomial.eq_C_of_degree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 0) : p = Polynomial.C (p.coeff 0)
• Polynomial.degree_C_mul_of_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (Polynomial.C a * p).degree = p.degree
• Polynomial.degree_mul_C_of_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Semiring R] (ha : IsUnit a) (p : Polynomial R) : (p * Polynomial.C a).degree = p.degree
• Polynomial.degree_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (p : Polynomial R) (n : ℕ) : (p ^ n).degree = n • p.degree
• Polynomial.degree_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] (a : R) : (Polynomial.X + Polynomial.C a).degree = 1
• Polynomial.eq_C_of_degree_le_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 0) : p = Polynomial.C (p.coeff 0)
• Polynomial.degree_le_zero_iff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : p.degree ≤ 0 ↔ p = Polynomial.C (p.coeff 0)
• Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).degree = max p.degree q.degree
• Polynomial.degree_mul' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).degree = p.degree + q.degree
• Polynomial.degree_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) : (p * Polynomial.X ^ n).degree = p.degree + ↑n
• Polynomial.degree_smul_of_isRightRegular_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (ha : a ≠ 0) (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree
• Polynomial.leadingCoeff_sub_of_degree_lt' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p - q).leadingCoeff = -q.leadingCoeff
• Polynomial.leadingCoeff_add_of_degree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
• Polynomial.degree_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.leadingCoeff ^ n ≠ 0 → (p ^ n).degree = n • p.degree
• Polynomial.degree_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : 0 < p.degree) : (p + Polynomial.C a).degree = p.degree
• Polynomial.leadingCoeff_sub_of_degree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff ≠ q.leadingCoeff) : (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
• Polynomial.degree_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] (a : R) : (Polynomial.X - Polynomial.C a).degree = 1
• Polynomial.degree_X_pow_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : (Polynomial.X ^ n + Polynomial.C a).degree = ↑n
• Polynomial.degree_C_lt_degree_C_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b).degree < (Polynomial.C a * Polynomial.X).degree
• Polynomial.degree_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Ring R] {p : Polynomial R} (hp : 0 < p.degree) : (p - Polynomial.C a).degree = p.degree
• Polynomial.degree_sum_fin_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {n : ℕ} (f : Fin n → R) : (∑ i, Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n
• Polynomial.degree_X_pow_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) : (Polynomial.X ^ n - Polynomial.C a).degree = ↑n
• Polynomial.le_degree_of_mem_supp 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → ↑a ≤ p.degree
• Polynomial.sum_fin 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {n : ℕ} {p : Polynomial R} (hn : p.degree < ↑n) : ∑ i, f (↑i) (p.coeff ↑i) = p.sum f
• Polynomial.degree_le_of_dvd 📋 Mathlib.Algebra.Polynomial.Degree.Domain
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) : p.degree ≤ q.degree
• Polynomial.eq_zero_of_dvd_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Domain
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h₁ : p ∣ q) (h₂ : q.degree < p.degree) : q = 0
• Polynomial.not_dvd_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Domain
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q
• Polynomial.le_natDegree_of_coe_le_degree 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree
• Polynomial.ne_zero_of_coe_le_degree 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : p ≠ 0
• Polynomial.zero_le_degree_iff 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : 0 ≤ p.degree ↔ p ≠ 0
• Polynomial.degree_linear_le 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1
• Polynomial.degree_linear 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree = 1
• Polynomial.eq_X_add_C_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 1) : p = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.C (p.coeff 0)
• Polynomial.degree_linear_lt 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2
• Polynomial.eq_X_add_C_of_degree_le_one 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
• Polynomial.degree_linear_lt_degree_C_mul_X_sq 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b * Polynomial.X + Polynomial.C c).degree < (Polynomial.C a * Polynomial.X ^ 2).degree
• Polynomial.degree_quadratic_le 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2
• Polynomial.degree_quadratic_lt 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3
• Polynomial.degree_quadratic 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2
• Polynomial.degree_quadratic_lt_degree_C_mul_X_cb 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < (Polynomial.C a * Polynomial.X ^ 3).degree
• Polynomial.degree_cubic_le 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3
• Polynomial.degree_cubic_lt 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < 4
• Polynomial.degree_cubic 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree = 3
• Polynomial.degree_eq_zero_of_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R] (h : IsUnit p) : p.degree = 0
• Polynomial.not_isUnit_of_degree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.degree) : ¬IsUnit p
• Polynomial.degree_coe_units 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) : (↑u).degree = 0
• Polynomial.Monic.degree_pos_of_not_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) : 0 < p.degree
• Polynomial.degree_pos_of_not_isUnit_of_dvd_monic 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {a p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < a.degree
• Polynomial.degree_map_le 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).degree ≤ p.degree
• Polynomial.degree_map_eq_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).degree = p.degree
• Polynomial.degree_map_lt 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (Polynomial.map f p).degree < p.degree
• MvPolynomial.degree_optionEquivLeft 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} (h : f ≠ 0) : ((MvPolynomial.optionEquivLeft R σ) f).degree = ↑(MvPolynomial.degreeOf none f)
• MvPolynomial.degree_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : ((MvPolynomial.finSuccEquiv R n) f).degree = ↑(MvPolynomial.degreeOf 0 f)
• Polynomial.coe_lt_degree 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : ↑n < p.degree ↔ n < p.natDegree
• Polynomial.degree_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Ring R] {p : Polynomial R} : (p.comp (-Polynomial.X)).degree = p.degree
• Polynomial.degree_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).degree = p.degree
• Polynomial.degree_pos_of_root 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (h : p.IsRoot a) : 0 < p.degree
• Polynomial.degree_map_eq_of_injective 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).degree = p.degree
• Polynomial.degree_map_eq_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
• Polynomial.degree_C_mul 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (Polynomial.C a * p).degree = p.degree
• Polynomial.degree_mul_C 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R] (a0 : a ≠ 0) : (p * Polynomial.C a).degree = p.degree
• Polynomial.degree_C_mul_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) : (Polynomial.C a * p).degree = p.degree
• Polynomial.degree_sum_eq_of_disjoint 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.degree ∘ f))) : (s.sum f).degree = s.sup fun i => (f i).degree
• Polynomial.degree_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (hq : 0 < q.degree) : (p.comp q).degree = p.degree * q.degree
• Polynomial.degree_pos_of_eval₂_root 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : 0 < p.degree
• Polynomial.degree_add_degree_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) : p.degree + (Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
• Polynomial.degree_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] {p : Polynomial K} (hp0 : p ≠ 0) : (Polynomial.C p.leadingCoeff⁻¹).degree = 0
• Polynomial.degree_mul_leadingCoeff_self_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) : (p * Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
• Polynomial.degree_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) : (p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
• Polynomial.eraseLead_degree_le 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.eraseLead.degree ≤ f.degree
• Polynomial.degree_eraseLead_lt 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f ≠ 0) : f.eraseLead.degree < f.degree
• Polynomial.eraseLead_add_of_degree_lt_left 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : q.degree < p.degree) : (p + q).eraseLead = p.eraseLead + q
• Polynomial.eraseLead_add_of_degree_lt_right 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : p.degree < q.degree) : (p + q).eraseLead = p + q.eraseLead
• Polynomial.Monic.degree_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).degree = P.degree
• Polynomial.Monic.add_of_left 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p + q).Monic
• Polynomial.Monic.add_of_right 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) (hpq : p.degree < q.degree) : (p + q).Monic
• Polynomial.Monic.degree_le_zero_iff_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1
• Polynomial.Monic.degree_mul_comm 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) : (p * q).degree = (q * p).degree
• Polynomial.degree_smul_of_smul_regular 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : (k • p).degree = p.degree
• Polynomial.Monic.sub_of_left 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p - q).Monic
• Polynomial.Monic.not_dvd_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q
• Polynomial.MonicDegreeEq.degree 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {n : ℕ} [Semiring R] [Nontrivial R] (p : Polynomial.MonicDegreeEq R n) : (↑p).degree = ↑n
• Polynomial.monic_X_pow_add 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (Polynomial.X ^ n + p).Monic
• Polynomial.Monic.sub_of_right 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.leadingCoeff = -1) (hpq : p.degree < q.degree) : (p - q).Monic
• Polynomial.monic_X_pow_sub 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (Polynomial.X ^ n - p).Monic
• Polynomial.degree_list_sum_le 📋 Mathlib.Algebra.Polynomial.BigOperators
  {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : l.sum.degree ≤ (List.map Polynomial.natDegree l).maximum
• Polynomial.degree_list_prod_le 📋 Mathlib.Algebra.Polynomial.BigOperators
  {S : Type u_1} [Semiring S] (l : List (Polynomial S)) : l.prod.degree ≤ (List.map Polynomial.degree l).sum
• Polynomial.degree_list_prod 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (l : List (Polynomial R)) : l.prod.degree = (List.map Polynomial.degree l).sum
• Polynomial.degree_multiset_prod_le 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) : t.prod.degree ≤ (Multiset.map Polynomial.degree t).sum
• Polynomial.degree_prod_le 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) : (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree
• Polynomial.degree_list_sum_le_of_forall_degree_le 📋 Mathlib.Algebra.Polynomial.BigOperators
  {S : Type u_1} [Semiring S] (l : List (Polynomial S)) (n : WithBot ℕ) (hl : ∀ p ∈ l, p.degree ≤ n) : l.sum.degree ≤ n
• Polynomial.degree_prod 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) [Nontrivial R] : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
• Polynomial.degree_multiset_prod 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) [Nontrivial R] : t.prod.degree = (Multiset.map (fun f => f.degree) t).sum
• Polynomial.degree_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
• Polynomial.degree_multiset_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) [Nontrivial R] (h : ∀ f ∈ t, f.Monic) : t.prod.degree = (Multiset.map Polynomial.degree t).sum
• Polynomial.leadingCoeff_sum_of_degree_eq 📋 Mathlib.Algebra.Polynomial.BigOperators
  {ι : Type w} {S : Type u_1} [Semiring S] {f : ι → Polynomial S} {s : Finset ι} {d : WithBot ℕ} (hd : ∀ k ∈ s, (f k).degree = d) (hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0) : (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff
• Polynomial.degree_sum_eq_of_linearIndepOn 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] {f : ι → Polynomial R} {v : ι → A} (h : LinearIndepOn R v ↑s) : (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).degree = s.sup fun i => (f i).degree
• Polynomial.Monic.geom_sum' 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic
• Polynomial.mem_degreeLE 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {n : WithBot ℕ} {f : Polynomial R} : f ∈ Polynomial.degreeLE R n ↔ f.degree ≤ n
• Polynomial.mem_degreeLT 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} {f : Polynomial R} : f ∈ Polynomial.degreeLT R n ↔ f.degree < ↑n
• Polynomial.degree_restriction 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Ring R] {p : Polynomial R} : p.restriction.degree = p.degree
• Polynomial.exists_degree_le_of_mem_span 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {s : Set (Polynomial R)} {p : Polynomial R} (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) : ∃ p' ∈ s, p.degree ≤ p'.degree
• Polynomial.exists_degree_le_of_mem_span_of_finite 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) (hs : s.Nonempty) : ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
• Ideal.mem_leadingCoeffNth 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (n : ℕ) (x : R) : x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
• Polynomial.degree_derivative_le 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} : (Polynomial.derivative p).degree ≤ p.degree
• Polynomial.degree_derivative_lt 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : (Polynomial.derivative p).degree < p.degree

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59