Loogle!

Result

Found 1031 declarations mentioning Polynomial.X. Of these, only the first 200 are shown.

• Polynomial.X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R
• Polynomial.commute_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : Commute Polynomial.X p
• Polynomial.X_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X ≠ 0
• Polynomial.support_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.support = {1}
• Polynomial.toFinsupp_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.X.toFinsupp = AddMonoidAlgebra.single 1 1
• Polynomial.support_X_empty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (H : 1 = 0) : Polynomial.X.support = ∅
• Polynomial.coeff_X_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.X.coeff 0 = 0
• Polynomial.commute_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : Commute (Polynomial.X ^ n) p
• 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.support_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (Polynomial.X ^ n).support = {n}
• Polynomial.X_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.X * p = p * Polynomial.X
• Polynomial.X_ne_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (a : R) : Polynomial.X ≠ Polynomial.C a
• Polynomial.toFinsupp_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n 1
• Polynomial.sum_X_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {f : ℕ → R → S} (hf : f 1 0 = 0) : Polynomial.X.sum f = f 1 1
• 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.toFinsupp_C_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).toFinsupp = AddMonoidAlgebra.single 1 a
• Polynomial.support_C_mul_X' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c * Polynomial.X).support ⊆ {1}
• Polynomial.support_C_mul_X_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c * Polynomial.X).support ⊆ {1}
• Polynomial.support_C_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {c : R} (h : c ≠ 0) : (Polynomial.C c * Polynomial.X).support = {1}
• Polynomial.monomial_one_one_eq_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (Polynomial.monomial 1) 1 = Polynomial.X
• Polynomial.toFinsupp_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n a
• Polynomial.X_pow_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : Polynomial.X ^ n * p = p * Polynomial.X ^ n
• Polynomial.support_C_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• Polynomial.support_C_mul_X_pow_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• Polynomial.sum_C_mul_X_pow_eq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : (p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
• Polynomial.support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) {c : R} (h : c ≠ 0) : (Polynomial.C c * Polynomial.X ^ n).support = {n}
• Polynomial.X_mul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (r : R) : Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X
• Polynomial.X_pow_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.X ^ n = (Polynomial.monomial n) 1
• Polynomial.monomial_one_right_eq_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.monomial n) 1 = Polynomial.X ^ n
• Polynomial.X_pow_mul_assoc 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} : p * Polynomial.X ^ n * q = p * q * Polynomial.X ^ n
• Polynomial.C_mul_X_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
• Polynomial.smul_X_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] {n : ℕ} : a • Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.C_mul_X_pow_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] {n : ℕ} : Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.X_pow_mul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (r : R) (n : ℕ) : Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n
• Polynomial.X_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : Polynomial.X * (Polynomial.monomial n) r = (Polynomial.monomial (n + 1)) r
• Polynomial.monomial_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : (Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
• Polynomial.X_pow_mul_assoc_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (r : R) : p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n
• Polynomial.X_pow_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k n : ℕ) (r : R) : Polynomial.X ^ k * (Polynomial.monomial n) r = (Polynomial.monomial (n + k)) r
• Polynomial.monomial_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
• Polynomial.support_binomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
• Polynomial.support_binomial_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
• Polynomial.ofMultiset_apply 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [CommRing R] (s : Multiset R) : Polynomial.ofMultiset s = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod
• Polynomial.induction_on 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R) (C : ∀ (a : R), motive (Polynomial.C a)) (add : ∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) (monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * Polynomial.X ^ n) → motive (Polynomial.C a * Polynomial.X ^ (n + 1))) : motive p
• Polynomial.support_trinomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
• Polynomial.support_trinomial_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
• Polynomial.binomial_eq_binomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) : Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ l = Polynomial.C u * Polynomial.X ^ m + Polynomial.C v * Polynomial.X ^ n ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
• Polynomial.eval_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {x : R} : Polynomial.eval x Polynomial.X = x
• Polynomial.X_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.X.comp p = p
• Polynomial.comp_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp Polynomial.X = p
• Polynomial.eval₂_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x Polynomial.X = x
• Polynomial.map_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f Polynomial.X = Polynomial.X
• Polynomial.eval_mul_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (p * Polynomial.X) = Polynomial.eval x p * x
• Polynomial.eval_X_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {x : R} (n : ℕ) : Polynomial.eval x (Polynomial.X ^ n) = x ^ n
• Polynomial.mul_X_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p r : Polynomial R} : (p * Polynomial.X).comp r = p.comp r * r
• Polynomial.eval₂_X_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (Polynomial.X * p) = Polynomial.eval₂ f x p * x
• Polynomial.eval₂_mul_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (p * Polynomial.X) = Polynomial.eval₂ f x p * x
• Polynomial.eval₂_X_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) {n : ℕ} : Polynomial.eval₂ f x (Polynomial.X ^ n) = x ^ n
• Polynomial.X_pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {k : ℕ} : (Polynomial.X ^ k).comp p = p ^ k
• Polynomial.eval_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {k : ℕ} : Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k
• Polynomial.root_X_sub_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a b : R} [Ring R] : (Polynomial.X - Polynomial.C a).IsRoot b ↔ a = b
• Polynomial.eval_geom_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [CommSemiring R] {n : ℕ} {x : R} : Polynomial.eval x (∑ i ∈ Finset.range n, Polynomial.X ^ i) = ∑ i ∈ Finset.range n, x ^ i
• Polynomial.mul_X_add_natCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)
• Polynomial.mul_X_pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p r : Polynomial R} {k : ℕ} : (p * Polynomial.X ^ k).comp r = p.comp r * r ^ k
• Polynomial.mul_comp_neg_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} [Ring R] (p q : Polynomial R) : (p * q).comp (-Polynomial.X) = p.comp (-Polynomial.X) * q.comp (-Polynomial.X)
• Polynomial.mul_X_sub_intCast_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)
• Polynomial.isRegular_X 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] : IsRegular Polynomial.X
• Polynomial.isRegular_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (n : ℕ) : IsRegular (Polynomial.X ^ n)
• 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.mul_X_pow_eq_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p * Polynomial.X ^ n = 0) : p = 0
• 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_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_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_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.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_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_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_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.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.card_support_binomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
• Polynomial.support_binomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
• Polynomial.one_add_X_pow_sub_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {S : Type u_1} [CommRing S] (d : ℕ) : (1 + Polynomial.X) ^ d - Polynomial.X ^ d = ∑ i ∈ Finset.range d, d.choose i • Polynomial.X ^ i
• Polynomial.card_support_trinomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support.card = 3
• Polynomial.support_trinomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support = {k, m, n}
• Polynomial.monic_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.Monic
• Polynomial.natDegree_X_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.natDegree ≤ 1
• Polynomial.natDegree_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.natDegree = 1
• Polynomial.degree_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.degree = 1
• Polynomial.leadingCoeff_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.leadingCoeff = 1
• Polynomial.degree_X_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.degree ≤ 1
• Polynomial.monic_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).Monic
• Polynomial.natDegree_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (Polynomial.X ^ n).natDegree = n
• Polynomial.degree_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (Polynomial.X ^ n).degree = ↑n
• Polynomial.degree_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).degree ≤ ↑n
• Polynomial.leadingCoeff_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).leadingCoeff = 1
• Polynomial.leadingCoeff_C_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).leadingCoeff = a
• 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.natDegree_C_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X).natDegree = 1
• 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.leadingCoeff_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a
• Polynomial.natDegree_C_mul_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n
• Polynomial.natDegree_X_sub_C_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (r : R) : (Polynomial.X - Polynomial.C r).natDegree ≤ 1
• 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.natDegree_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) (a : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).natDegree = n
• 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.not_isUnit_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] : ¬IsUnit Polynomial.X
• Polynomial.leadingCoeff_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : (p * Polynomial.X).leadingCoeff = p.leadingCoeff
• Polynomial.natDegree_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u_1} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).natDegree ≤ n
• 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_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.leadingCoeff_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (p * Polynomial.X ^ n).leadingCoeff = p.leadingCoeff
• Polynomial.natDegree_X_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p ≠ 0) : (Polynomial.X * p).natDegree = p.natDegree + 1
• Polynomial.natDegree_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p ≠ 0) : (p * Polynomial.X).natDegree = p.natDegree + 1
• Polynomial.nextCoeff_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {S : Type v} [Semiring S] (c : S) : (Polynomial.X + Polynomial.C c).nextCoeff = c
• Polynomial.natDegree_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] (x : R) : (Polynomial.X + Polynomial.C x).natDegree = 1
• Polynomial.X_add_C_ne_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] (r : R) : Polynomial.X + Polynomial.C r ≠ 1
• Polynomial.X_add_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] (r : R) : Polynomial.X + Polynomial.C r ≠ 0
• 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.leadingCoeff_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {S : Type v} [Semiring S] (r : S) : (Polynomial.X + Polynomial.C r).leadingCoeff = 1
• 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.leadingCoeff_X_pow_add_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {n : ℕ} (hn : 0 < n) : (Polynomial.X ^ n + 1).leadingCoeff = 1
• Polynomial.natDegree_X_pow_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) (hp : p ≠ 0) : (Polynomial.X ^ n * p).natDegree = p.natDegree + n
• Polynomial.natDegree_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) (hp : p ≠ 0) : (p * Polynomial.X ^ n).natDegree = p.natDegree + n
• Polynomial.natDegree_X_pow_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} {r : R} : (Polynomial.X ^ n + Polynomial.C r).natDegree = n
• Polynomial.zero_notMem_multiset_map_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] {α : Type u_1} (m : Multiset α) (f : α → R) : 0 ∉ Multiset.map (fun a => Polynomial.X + Polynomial.C (f a)) m
• Polynomial.natDegree_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] (x : R) : (Polynomial.X - Polynomial.C x).natDegree = 1
• Polynomial.leadingCoeff_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {S : Type v} [Ring S] (r : S) : (Polynomial.X - Polynomial.C r).leadingCoeff = 1
• Polynomial.leadingCoeff_pow_X_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] (r : R) (i : ℕ) : ((Polynomial.X + Polynomial.C r) ^ i).leadingCoeff = 1
• 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.nextCoeff_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {S : Type v} [Ring S] (c : S) : (Polynomial.X - Polynomial.C c).nextCoeff = -c
• 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.X_sub_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] (r : R) : Polynomial.X - Polynomial.C r ≠ 0
• Polynomial.X_pow_add_C_ne_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : Polynomial.X ^ n + Polynomial.C a ≠ 1
• Polynomial.X_pow_add_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Nontrivial R] [Semiring R] {n : ℕ} (hn : 0 < n) (a : R) : Polynomial.X ^ n + Polynomial.C a ≠ 0
• Polynomial.leadingCoeff_X_pow_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {n : ℕ} (hn : 0 < n) {r : R} : (Polynomial.X ^ n + Polynomial.C r).leadingCoeff = 1
• Polynomial.leadingCoeff_X_pow_sub_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {n : ℕ} (hn : 0 < n) : (Polynomial.X ^ n - 1).leadingCoeff = 1
• 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_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.zero_notMem_multiset_map_X_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] {α : Type u_1} (m : Multiset α) (f : α → R) : 0 ∉ Multiset.map (fun a => Polynomial.X - Polynomial.C (f a)) m
• Polynomial.natDegree_X_pow_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} {r : R} : (Polynomial.X ^ n - Polynomial.C r).natDegree = 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.leadingCoeff_X_pow_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {n : ℕ} (hn : 0 < n) {r : R} : (Polynomial.X ^ n - Polynomial.C r).leadingCoeff = 1
• Polynomial.X_pow_sub_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) : Polynomial.X ^ n - Polynomial.C a ≠ 0
• 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.card_support_C_mul_X_pow_le_one 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {c : R} {n : ℕ} : (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1
• Polynomial.mem_support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {n a : ℕ} {c : R} (h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support) : a = n
• 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_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.natDegree_linear_le 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1
• Polynomial.leadingCoeff_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).leadingCoeff = a
• 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.natDegree_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).natDegree = 1
• Polynomial.exists_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) : ∃ a b, p = Polynomial.C a * Polynomial.X + Polynomial.C b
• 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.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_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.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.natDegree_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).natDegree ≤ 2
• Polynomial.leadingCoeff_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).leadingCoeff = a
• Polynomial.natDegree_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).natDegree = 2
• 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.natDegree_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).natDegree ≤ 3
• Polynomial.leadingCoeff_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).leadingCoeff = a
• Polynomial.natDegree_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).natDegree = 3
• 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.eval₂_C_X 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.eval₂ Polynomial.C Polynomial.X p = p
• Polynomial.comp_C_mul_X_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} [Semiring R] {p : Polynomial R} {r : R} (hr : r ∈ nonZeroDivisors R) : p.comp (Polynomial.C r * Polynomial.X) = 0 ↔ p = 0
• 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.ringHom_ext' 📋 Mathlib.Algebra.Polynomial.Monomial
  {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f g : Polynomial R →+* S} (h₁ : f.comp Polynomial.C = g.comp Polynomial.C) (h₂ : f Polynomial.X = g Polynomial.X) : f = g
• Polynomial.ringHom_ext'_iff 📋 Mathlib.Algebra.Polynomial.Monomial
  {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f g : Polynomial R →+* S} : f = g ↔ f.comp Polynomial.C = g.comp Polynomial.C ∧ f Polynomial.X = g Polynomial.X
• Polynomial.ringHom_ext 📋 Mathlib.Algebra.Polynomial.Monomial
  {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f g : Polynomial R →+* S} (h₁ : ∀ (a : R), f (Polynomial.C a) = g (Polynomial.C a)) (h₂ : f Polynomial.X = g Polynomial.X) : f = g
• Polynomial.comp_neg_X_comp_neg_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (p : Polynomial R) : (p.comp (-Polynomial.X)).comp (-Polynomial.X) = p
• Polynomial.aeval_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) Polynomial.X = x
• Polynomial.algEquivOfCompEqX 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) : Polynomial R ≃ₐ[R] Polynomial R
• Polynomial.aeval_X_left 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] : Polynomial.aeval Polynomial.X = AlgHom.id R (Polynomial R)
• Polynomial.comp_X_add_C_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [Semiring S] {p : Polynomial S} {t : S} : p.comp (Polynomial.X + Polynomial.C t) = 0 ↔ p = 0
• Polynomial.comp_X_add_C_ne_zero_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [Semiring S] {p : Polynomial S} {t : S} : p.comp (Polynomial.X + Polynomial.C t) ≠ 0 ↔ p ≠ 0
• Polynomial.not_isUnit_X_sub_C 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [Ring R] [Nontrivial R] (r : R) : ¬IsUnit (Polynomial.X - Polynomial.C r)
• Polynomial.aevalTower_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') : (Polynomial.aevalTower g y) Polynomial.X = y
• Polynomial.X_mem_nonzeroDivisors 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] : Polynomial.X ∈ nonZeroDivisors (Polynomial R)
• Polynomial.eval₂_intCastRingHom_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [Ring R] (p : Polynomial ℤ) (f : Polynomial ℤ →+* R) : Polynomial.eval₂ (Int.castRingHom R) (f Polynomial.X) p = f p
• Polynomial.aeval_X_left_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p : Polynomial R) : (Polynomial.aeval Polynomial.X) p = p
• Polynomial.eval_mul_X_sub_C 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [Ring R] {p : Polynomial R} (r : R) : Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 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