Loogle!

Result

Found 545 declarations mentioning Polynomial.coeff. Of these, only the first 200 are shown.

• Polynomial.coeff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R → ℕ →₀ R
• Polynomial.coeff_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Function.Injective Polynomial.coeff
• Polynomial.coeff_ofFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) : { toFinsupp := p }.coeff = p.coeff
• Polynomial.coeff_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p.coeff = q.coeff ↔ p = q
• Polynomial.finite_range_coeff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (f : Polynomial R) : (Set.range ⇑f.coeff).Finite
• Polynomial.coeff_update_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p.update n a).coeff n = a
• Polynomial.coeff_X_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.X.coeff 0 = 0
• Polynomial.erase_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).coeff n = 0
• Polynomial.coeff_X_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.X.coeff 1 = 1
• Polynomial.coeff_X_of_ne_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 1) : Polynomial.X.coeff n = 0
• Polynomial.coeff_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.coeff 0) n = 0
• Polynomial.sum_def 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
• Polynomial.coeff_one_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (Polynomial.coeff 1) 0 = 1
• Polynomial.mem_support_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∈ p.support ↔ p.coeff n ≠ 0
• Polynomial.notMem_support_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∉ p.support ↔ p.coeff n = 0
• Polynomial.toFinsupp_apply 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (f : Polynomial R) (i : ℕ) : f.toFinsupp.coeff i = f.coeff i
• Polynomial.coeff_ofNat_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).coeff 0 = OfNat.ofNat a
• Polynomial.erase_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) {n i : ℕ} (h : i ≠ n) : (Polynomial.erase n p).coeff i = p.coeff i
• Polynomial.ext 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
• Polynomial.ext_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
• Polynomial.coeff_ofNat_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a n : ℕ) [h : a.AtLeastTwo] : (OfNat.ofNat a).coeff (n + 1) = 0
• Polynomial.coeff_update_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) {n i : ℕ} (a : R) (h : i ≠ n) : (p.update n a).coeff i = p.coeff i
• Polynomial.mem_coeffs_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n
• Polynomial.coeff_update 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : ⇑(p.update n a).coeff = Function.update (⇑p.coeff) n a
• Polynomial.coeff_natCast_ite 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {m n : ℕ} [Semiring R] : (↑m).coeff n = ↑(if n = 0 then m else 0)
• Polynomial.coeff_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] : Polynomial.X.coeff n = if 1 = n then 1 else 0
• Polynomial.coeff_C_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).coeff 0 = a
• Polynomial.coeff_update_apply 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ) : (p.update n a).coeff i = if i = n then a else p.coeff i
• Polynomial.coeff_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) : (Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
• Polynomial.coeff_mem_coeffs 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs
• Polynomial.coeff_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} : (Polynomial.coeff 1) n = if n = 0 then 1 else 0
• Polynomial.coeff_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) : (Polynomial.C a).coeff n = 0
• Polynomial.coeff_C_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) : (Polynomial.C a).coeff n = 0
• Polynomial.coeff_C_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {r : R} {n : ℕ} : (Polynomial.C r).coeff (n + 1) = 0
• Polynomial.coeff_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (p : Polynomial R) (n : ℕ) : (-p).coeff n = -p.coeff n
• Polynomial.coeff_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : (Polynomial.C a).coeff n = if n = 0 then a else 0
• Polynomial.sum_eq_of_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {p : Polynomial R} (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {s : Finset ℕ} (hs : p.support ⊆ s) : p.sum f = ∑ n ∈ s, f n (p.coeff n)
• Polynomial.coeff_monomial_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : ((Polynomial.monomial n) c).coeff n = c
• Polynomial.coeff_monomial_of_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {m n : ℕ} (c : R) (h : m ≠ n) : ((Polynomial.monomial n) c).coeff m = 0
• Polynomial.coeff_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {m n : ℕ} [Semiring R] : ((Polynomial.monomial n) a).coeff m = if n = m then a else 0
• Polynomial.coeff_monomial_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : ((Polynomial.monomial (n + 1)) a).coeff 0 = 0
• Polynomial.monomial_add_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.monomial n) (p.coeff n) + Polynomial.erase n p = p
• Polynomial.coeff_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (p q : Polynomial R) (n : ℕ) : (p - q).coeff n = p.coeff n - q.coeff n
• Polynomial.mul_eq_sum_sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p * q = ∑ i ∈ p.support, q.sum fun j a => (Polynomial.monomial (i + j)) (p.coeff i * a)
• Polynomial.eval₂_mul_noncomm 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x) : Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
• Polynomial.eval₂_list_prod_noncomm 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (ps : List (Polynomial R)) (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) : Polynomial.eval₂ f x ps.prod = (List.map (Polynomial.eval₂ f x) ps).prod
• Polynomial.natCast_coeff_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {n : ℕ} {R : Type u_1} [Semiring R] : (↑n).coeff 0 = ↑n
• Polynomial.intCast_coeff_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {i : ℤ} {R : Type u_1} [Ring R] : (↑i).coeff 0 = ↑i
• Polynomial.coeff_X_mul_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) : (Polynomial.X * p).coeff 0 = 0
• Polynomial.coeff_mul_X_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) : (p * Polynomial.X).coeff 0 = 0
• Polynomial.coeff_X_pow_self 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).coeff n = 1
• Polynomial.constantCoeff_apply 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.constantCoeff p = p.coeff 0
• Polynomial.finsetSum_coeff 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ) : (∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n
• Polynomial.finset_sum_coeff 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) (n : ℕ) : (∑ b ∈ s, f b).coeff n = ∑ b ∈ s, (f b).coeff n
• Polynomial.coeff_X_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.X * p).coeff (n + 1) = p.coeff n
• Polynomial.coeff_mul_X 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p * Polynomial.X).coeff (n + 1) = p.coeff n
• Polynomial.coeff_sum 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (n : ℕ) (f : ℕ → R → Polynomial S) : (p.sum f).coeff n = p.sum fun a b => (f a b).coeff n
• Polynomial.coeff_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (k n : ℕ) : (Polynomial.X ^ k).coeff n = if n = k then 1 else 0
• Polynomial.coeff_list_sum_map 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {ι : Type u_1} (l : List ι) (f : ι → Polynomial R) (n : ℕ) : (List.map f l).sum.coeff n = (List.map (fun a => (f a).coeff n) l).sum
• Polynomial.coeff_X_add_one_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  (R : Type u_1) [Semiring R] (n k : ℕ) : ((Polynomial.X + 1) ^ n).coeff k = ↑(n.choose k)
• Polynomial.coeff_one_add_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  (R : Type u_1) [Semiring R] (n k : ℕ) : ((1 + Polynomial.X) ^ n).coeff k = ↑(n.choose k)
• Polynomial.coeff_mul_natCast 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} : (p * ↑a).coeff k = p.coeff k * ↑a
• Polynomial.coeff_natCast_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} : (↑a * p).coeff k = ↑a * p.coeff k
• Polynomial.C_dvd_iff_dvd_coeff 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (r : R) (φ : Polynomial R) : Polynomial.C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i
• Polynomial.coeff_smul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} {S : Type v} [Semiring R] [SMulZeroClass S R] (r : S) (p : Polynomial R) (n : ℕ) : (r • p).coeff n = r • p.coeff n
• Polynomial.coeff_add 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p q : Polynomial R) (n : ℕ) : (p + q).coeff n = p.coeff n + q.coeff n
• Polynomial.coeff_X_pow_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (Polynomial.X ^ n * p).coeff (d + n) = p.coeff d
• Polynomial.coeff_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
• Polynomial.lcoeff_apply 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (n : ℕ) (f : Polynomial R) : (Polynomial.lcoeff R n) f = f.coeff n
• Polynomial.coeff_C_mul_X 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (x : R) (n : ℕ) : (Polynomial.C x * Polynomial.X).coeff n = if n = 1 then x else 0
• Polynomial.coeff_mul_ofNat 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} [a.AtLeastTwo] : (p * OfNat.ofNat a).coeff k = p.coeff k * OfNat.ofNat a
• Polynomial.coeff_ofNat_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} {a k : ℕ} [a.AtLeastTwo] : (OfNat.ofNat a * p).coeff k = OfNat.ofNat a * p.coeff k
• Polynomial.mul_coeff_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).coeff 0 = p.coeff 0 * q.coeff 0
• Polynomial.coeff_C_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (p : Polynomial R) : (Polynomial.C a * p).coeff n = a * p.coeff n
• Polynomial.coeff_mul_C 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p * Polynomial.C a).coeff n = p.coeff n * a
• Polynomial.coeff_intCast_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} : (↑a * p).coeff k = ↑a * p.coeff k
• Polynomial.coeff_mul_intCast 📋 Mathlib.Algebra.Polynomial.Coeff
  {S : Type v} [Ring S] {p : Polynomial S} {a : ℤ} {k : ℕ} : (p * ↑a).coeff k = p.coeff k * ↑a
• Polynomial.coeff_X_pow_mul' 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (Polynomial.X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0
• Polynomial.coeff_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) : (p * Polynomial.X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0
• Polynomial.coeff_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p q : Polynomial R) (n : ℕ) : (p * q).coeff n = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, p.coeff x.1 * q.coeff x.2
• Polynomial.coeff_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (x : R) (k n : ℕ) : (Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
• Polynomial.coeff_list_sum 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (l : List (Polynomial R)) (n : ℕ) : l.sum.coeff n = (List.map (⇑(Polynomial.lcoeff R n)) l).sum
• Polynomial.coeff_X_add_C_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (r : R) (n k : ℕ) : ((Polynomial.X + Polynomial.C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)
• Polynomial.coeff_monomial_zero_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) : ((Polynomial.monomial 0) r * p).coeff d = r * p.coeff d
• Polynomial.coeff_mul_monomial_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) : (p * (Polynomial.monomial 0) r).coeff d = p.coeff d * r
• Polynomial.coeff_monomial_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) (r : R) : ((Polynomial.monomial n) r * p).coeff (d + n) = r * p.coeff d
• Polynomial.coeff_mul_monomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) (r : R) : (p * (Polynomial.monomial n) r).coeff (d + n) = p.coeff d * r
• Polynomial.mul_coeff_one 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
• Polynomial.update_eq_add_sub_coeff 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u_1} [Ring R] (p : Polynomial R) (n : ℕ) (a : R) : p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
• Polynomial.coeff_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natDegree = p.leadingCoeff
• Polynomial.Monic.coeff_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.coeff p.natDegree = 1
• 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.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.nextCoeff_of_natDegree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : 0 < p.natDegree) : p.nextCoeff = p.coeff (p.natDegree - 1)
• 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_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_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.nextCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0
• Polynomial.nextCoeff_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
• Polynomial.coeff_eq_zero_of_natDegree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.natDegree < n) : p.coeff n = 0
• Polynomial.le_natDegree_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : n ≤ p.natDegree
• Polynomial.coeff_natDegree_succ_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff (p.natDegree + 1) = 0
• Polynomial.natDegree_eq_of_le_of_coeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) (p1 : p.coeff n ≠ 0) : p.natDegree = n
• Polynomial.monic_of_natDegree_le_of_coeff_eq_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) : p.Monic
• 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.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.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.coeff_mul_degree_add_degree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] (p q : Polynomial R) : (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff
• Polynomial.eq_C_of_natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree = 0) : p = Polynomial.C (p.coeff 0)
• Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : p = Polynomial.C (p.coeff 0) ↔ p.natDegree = 0
• Polynomial.eq_C_of_natDegree_le_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 0) : p = Polynomial.C (p.coeff 0)
• Polynomial.ext_iff_natDegree_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) : p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i
• Polynomial.coeff_pow_mul_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
• 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.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.ite_le_natDegree_coeff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (I : Decidable (n < 1 + p.natDegree)) : (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n
• 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.coeff_mul_add_eq_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {df dg : ℕ} {f g : Polynomial R} (hdf : f.natDegree ≤ df) (hdg : g.natDegree ≤ dg) : (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
• Polynomial.coeff_X_sub_C_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p : Polynomial R} {r : R} {a : ℕ} : ((Polynomial.X - Polynomial.C r) * p).coeff (a + 1) = p.coeff a - r * p.coeff (a + 1)
• Polynomial.coeff_mul_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p : Polynomial R} {r : R} {a : ℕ} : (p * (Polynomial.X - Polynomial.C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r
• Polynomial.sum_over_range' 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) (n : ℕ) (hn : p.natDegree < n) : p.sum f = ∑ a ∈ Finset.range n, f a (p.coeff a)
• Polynomial.sum_over_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) : p.sum f = ∑ a ∈ Finset.range (p.natDegree + 1), f a (p.coeff a)
• 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.as_sum_support 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i)
• Polynomial.as_sum_range' 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (hn : p.natDegree < n) : p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)
• Polynomial.as_sum_support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.as_sum_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff i)
• Polynomial.as_sum_range_C_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) {n : ℕ} (hn : p.natDegree < n) : p = ∑ i ∈ Finset.range n, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.as_sum_range_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.Monic.eq_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 1) : p = Polynomial.X + Polynomial.C (p.coeff 0)
• 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.eq_X_add_C_of_natDegree_le_one 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
• 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.coeff_coe_units_zero_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) : (↑u).coeff 0 ≠ 0
• Polynomial.coeff_zero_eq_eval_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) : p.coeff 0 = Polynomial.eval 0 p
• Polynomial.coeff_zero_eq_zero_of_zero_isRoot 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.IsRoot 0 → p.coeff 0 = 0
• Polynomial.zero_isRoot_of_coeff_zero_eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff 0 = 0 → p.IsRoot 0
• Polynomial.zero_isRoot_iff_coeff_zero_eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : p.IsRoot 0 ↔ p.coeff 0 = 0
• Polynomial.eval₂_at_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) : Polynomial.eval₂ f 0 p = f (p.coeff 0)
• Polynomial.coeff_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ℕ) : (Polynomial.map f p).coeff n = f (p.coeff n)
• Polynomial.coeff_map_eq_comp 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : ⇑(Polynomial.map f p).coeff = ⇑f ∘ ⇑p.coeff
• Polynomial.eval_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
• Polynomial.eval_eq_sum_range 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
• Polynomial.coeff_comp_degree_mul_degree 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p q : Polynomial R} (hqd0 : q.natDegree ≠ 0) : (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
• Polynomial.eval₂_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
• Polynomial.eval₂_eq_sum_range 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
• Polynomial.comp_C_mul_X_coeff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} {r : R} {n : ℕ} : (p.comp (Polynomial.C r * Polynomial.X)).coeff n = p.coeff n * r ^ n
• Polynomial.coeff_zero_eq_aeval_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p : Polynomial R) : p.coeff 0 = (Polynomial.aeval 0) p
• Polynomial.coeff_zero_eq_aeval_zero' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) : (algebraMap R A) (p.coeff 0) = (Polynomial.aeval 0) p
• Polynomial.aeval_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i
• Polynomial.aeval_eq_sum_range 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i
• Polynomial.coeff_mapAlgHom_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (p : Polynomial A) (n : ℕ) : ((Polynomial.mapAlgHom f) p).coeff n = f (p.coeff n)
• Polynomial.mem_nonzeroDivisors_of_coeff_mem 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {p : Polynomial R} (n : ℕ) (hp : p.coeff n ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)
• Polynomial.dvd_term_of_isRoot_of_dvd_terms 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [CommRing S] {r p : S} {f : Polynomial S} (i : ℕ) (hr : f.IsRoot r) (h : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i
• Polynomial.dvd_term_of_dvd_eval_of_dvd_terms 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [CommRing S] {z p : S} {f : Polynomial S} (i : ℕ) (dvd_eval : p ∣ Polynomial.eval z f) (dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j) : p ∣ f.coeff i * z ^ i
• Polynomial.units_coeff_zero_smul 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R) : (↑c).coeff 0 • p = ↑c * p
• Polynomial.coeff_zero_of_isScalarTower 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {A : Type u_3} (B : Type u_4) (C : Type u_5) [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] (p : Polynomial A) : (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = ((Polynomial.mapAlg A C) p).coeff 0
• MvPolynomial.coeff_eval_eq_eval_coeff 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} (S₁ : Type v) [CommSemiring R] (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ) : (Polynomial.map (MvPolynomial.eval s') f).coeff i = (MvPolynomial.eval s') (f.coeff i)
• MvPolynomial.coeff_uniqueAlgEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] [Unique σ] (P : MvPolynomial σ R) (n : ℕ) : ((MvPolynomial.uniqueAlgEquiv R σ) P).coeff n = P.coeff fun₀ | default => n
• MvPolynomial.coeff_uniqueAlgEquiv_symm 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] [Unique σ] (P : Polynomial R) (d : σ →₀ ℕ) : ((MvPolynomial.uniqueAlgEquiv R σ).symm P).coeff d = P.coeff (d default)
• MvPolynomial.totalDegree_coeff_optionEquivLeft_le 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (p : MvPolynomial (Option S₁) R) (i : ℕ) : (((MvPolynomial.optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree
• MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (p : MvPolynomial (Option S₁) R) (i : ℕ) (hi : i ≤ p.totalDegree) : (((MvPolynomial.optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree
• MvPolynomial.mem_support_coeff_optionEquivLeft 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} {i : ℕ} {m : σ →₀ ℕ} : m ∈ (((MvPolynomial.optionEquivLeft R σ) f).coeff i).support ↔ Finsupp.optionElim i m ∈ f.support
• MvPolynomial.optionEquivLeft_coeff_coeff 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] (p : MvPolynomial (Option σ) R) (m : ℕ) (d : σ →₀ ℕ) : (((MvPolynomial.optionEquivLeft R σ) p).coeff m).coeff d = p.coeff (Finsupp.optionElim m d)
• MvPolynomial.optionEquivLeft_coeff_some_coeff_none 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) : (((MvPolynomial.optionEquivLeft R S₁) f).coeff (n none)).coeff n.some = f.coeff n
• MvPolynomial.degreeOf_coeff_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) : MvPolynomial.degreeOf j (((MvPolynomial.finSuccEquiv R n) p).coeff i) ≤ MvPolynomial.degreeOf j.succ p
• MvPolynomial.mem_support_coeff_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} : m ∈ (((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i m ∈ f.support
• MvPolynomial.finSuccEquiv_coeff_coeff 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) : (((MvPolynomial.finSuccEquiv R n) f).coeff i).coeff m = f.coeff (Finsupp.cons i m)
• MvPolynomial.mem_image_support_coeff_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin (n + 1) →₀ ℕ} : x ∈ Finsupp.cons i '' ↑(((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i
• MvPolynomial.image_support_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} : Finset.image (Finsupp.cons i) (((MvPolynomial.finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}
• MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) (hi : ((MvPolynomial.finSuccEquiv R n) f).coeff i ≠ 0) : (((MvPolynomial.finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
• Polynomial.coeff_eq_zero_of_lt_natTrailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n < p.natTrailingDegree) : p.coeff n = 0
• Polynomial.natTrailingDegree_le_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : p.natTrailingDegree ≤ n
• Polynomial.coeff_eq_zero_of_lt_trailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : ↑n < p.trailingDegree) : p.coeff n = 0
• Polynomial.trailingDegree_le_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (h : p.coeff n ≠ 0) : p.trailingDegree ≤ ↑n
• Polynomial.coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.trailingDegree < q.trailingDegree) : q.coeff p.natTrailingDegree = 0
• Polynomial.trailingDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingDegree = 0 ↔ p.coeff 0 ≠ 0
• Polynomial.trailingDegree_le_trailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.coeff p.natTrailingDegree ≠ 0) : q.trailingDegree ≤ p.trailingDegree
• Polynomial.trailingDegree_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.trailingDegree ≠ 0 ↔ p.coeff 0 = 0
• Polynomial.coeff_natTrailingDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natTrailingDegree = 0 ↔ p = 0
• Polynomial.coeff_natTrailingDegree_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natTrailingDegree ≠ 0 ↔ p ≠ 0
• Polynomial.coeff_natTrailingDegree_pred_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} {hp : 0 < ↑p.natTrailingDegree} : p.coeff (p.natTrailingDegree - 1) = 0
• Polynomial.le_natTrailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) : n ≤ p.natTrailingDegree
• Polynomial.natTrailingDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0
• Polynomial.natTrailingDegree_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p.natTrailingDegree ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
• Polynomial.trailingCoeff_eq_coeff_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.coeff 0 ≠ 0) : p.trailingCoeff = p.coeff 0
• Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p q : Polynomial R} : (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff
• Polynomial.nextCoeffUp_of_constantCoeff_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] (p : Polynomial R) (hp : p.coeff 0 = 0) : p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
• Polynomial.natDegree_le_iff_coeff_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
• Polynomial.coeff_add_eq_left_of_lt 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n
• Polynomial.coeff_add_eq_right_of_lt 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Semiring R] {p q : Polynomial R} (pn : p.natDegree < n) : (p + q).coeff n = q.coeff n
• Polynomial.natDegree_lt_coeff_mul 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {m n : ℕ} [Semiring R] {p q : Polynomial R} (h : p.natDegree + q.natDegree < m + n) : (p * q).coeff (m + n) = 0
• Polynomial.coeff_sub_eq_left_of_lt 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (dg : q.natDegree < n) : (p - q).coeff n = p.coeff n
• Polynomial.coeff_pow_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) : (p ^ m).coeff (m * n) = p.coeff n ^ m
• Polynomial.coeff_sub_eq_neg_right_of_lt 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Ring R] {p q : Polynomial R} (df : p.natDegree < n) : (p - q).coeff n = -q.coeff n
• Polynomial.natDegree_add_coeff_mul 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] (f g : Polynomial R) : (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
• Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {m n : ℕ} [Semiring R] {p : Polynomial R} {o : ℕ} (pn : p.natDegree ≤ n) (mno : m * n ≤ o) : (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
• Polynomial.comp_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : p.comp q = 0 ↔ p = 0 ∨ Polynomial.eval (q.coeff 0) p = 0 ∧ q = Polynomial.C (q.coeff 0)

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 ce5dd8c