Loogle!

Result

Found 932 declarations mentioning Polynomial.C. Of these, only the first 200 are shown.

• Polynomial.C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : R →+* Polynomial R
• Polynomial.C_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Function.Injective ⇑Polynomial.C
• Polynomial.X_ne_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (a : R) : Polynomial.X ≠ Polynomial.C a
• Polynomial.toFinsupp_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).toFinsupp = AddMonoidAlgebra.single 0 a
• Polynomial.C_eq_natCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.C ↑n = ↑n
• Polynomial.C_0 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.C 0 = 0
• Polynomial.support_C_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).support ⊆ {0}
• Polynomial.C_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.C 1 = 1
• Polynomial.C_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a = 0 ↔ a = 0
• Polynomial.C_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a ≠ 0 ↔ a ≠ 0
• Polynomial.support_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : R} (h : a ≠ 0) : (Polynomial.C a).support = {0}
• Polynomial.coeff_C_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).coeff 0 = a
• Polynomial.C_ofNat 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : Polynomial.C (OfNat.ofNat n) = OfNat.ofNat n
• 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.C_eq_intCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (n : ℤ) : Polynomial.C ↑n = ↑n
• 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.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.coeff_C_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {r : R} {n : ℕ} : (Polynomial.C r).coeff (n + 1) = 0
• Polynomial.C_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Semiring R] : Polynomial.C a = Polynomial.C b ↔ a = b
• 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.sum_C_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : R} {β : Type u_1} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (Polynomial.C a).sum f = f 0 a
• 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.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.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.C_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : Polynomial.C (a ^ n) = Polynomial.C a ^ n
• Polynomial.monomial_zero_left 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] ⦃a : R⦄ : (Polynomial.monomial 0) a = Polynomial.C a
• Polynomial.smul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (s : S) (r : R) : s • Polynomial.C r = Polynomial.C (s • r)
• 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.C_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Ring R] : Polynomial.C (-a) = -Polynomial.C a
• Polynomial.C_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Semiring R] : Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b
• Polynomial.C_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Semiring R] : Polynomial.C (a * b) = Polynomial.C a * Polynomial.C b
• Polynomial.nnqsmul_eq_C_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [DivisionSemiring R] (q : ℚ≥0) (f : Polynomial R) : q • f = Polynomial.C ↑q * f
• 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.qsmul_eq_C_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [DivisionRing R] (a : ℚ) (f : Polynomial R) : a • f = Polynomial.C ↑a * f
• 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.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.C_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Ring R] : Polynomial.C (a - b) = Polynomial.C a - Polynomial.C b
• Polynomial.C_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} {n : ℕ} [Semiring R] : Polynomial.C a * (Polynomial.monomial n) b = (Polynomial.monomial n) (a * b)
• Polynomial.monomial_mul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} {n : ℕ} [Semiring R] : (Polynomial.monomial n) a * Polynomial.C b = (Polynomial.monomial n) (a * b)
• 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_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {x : R} : Polynomial.eval x (Polynomial.C a) = a
• Polynomial.eval₂RingHom_comp_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) : (Polynomial.eval₂RingHom f x).comp Polynomial.C = f
• Polynomial.not_isRoot_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] (r a : R) (hr : r ≠ 0) : ¬(Polynomial.C r).IsRoot a
• Polynomial.comp_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp 0 = Polynomial.C (Polynomial.eval 0 p)
• Polynomial.comp_one 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.comp 1 = Polynomial.C (Polynomial.eval 1 p)
• Polynomial.mapRingHom_comp_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) : (Polynomial.mapRingHom f).comp Polynomial.C = Polynomial.C.comp f
• Polynomial.eval_C_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p
• Polynomial.eval₂_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (Polynomial.C a) = f a
• Polynomial.C_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : (Polynomial.C a).comp p = Polynomial.C a
• Polynomial.eval_mul_C_of_commute 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {x : R} (h : Commute a x) : Polynomial.eval x (p * Polynomial.C a) = Polynomial.eval x p * a
• Polynomial.comp_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : p.comp (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
• 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.comp_eq_sum_left 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p q : Polynomial R} : p.comp q = p.sum fun e a => Polynomial.C a * q ^ e
• Polynomial.map_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
• Polynomial.C_mul_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p r : Polynomial R} : (Polynomial.C a * p).comp r = Polynomial.C a * p.comp r
• Polynomial.eval₂_mul_C' 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) (h : Commute (f a) x) : Polynomial.eval₂ f x (p * Polynomial.C a) = Polynomial.eval₂ f x p * f a
• Polynomial.monomial_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ℕ) : ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
• Polynomial.isUnit_C 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {x : R} : IsUnit (Polynomial.C x) ↔ IsUnit x
• 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.C_mul' 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (a : R) (f : Polynomial R) : Polynomial.C a * f = a • f
• Polynomial.smul_eq_C_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} (a : R) : a • p = Polynomial.C a * p
• 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_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_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.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.leadingCoeff_C 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).leadingCoeff = a
• Polynomial.natDegree_C 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).natDegree = 0
• Polynomial.nextCoeff_C_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c).nextCoeff = 0
• Polynomial.Monic.ne_zero_of_C 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] {c : R} (hc : (Polynomial.C c).Monic) : c ≠ 0
• 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.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 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a).degree = 0
• 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.natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : p.natDegree = 0 ↔ ∃ x, Polynomial.C x = p
• 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_C_add 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {a : R} : (Polynomial.C a + p).natDegree = p.natDegree
• Polynomial.natDegree_add_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {a : R} : (p + Polynomial.C a).natDegree = p.natDegree
• Polynomial.Monic.leadingCoeff_C_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (Polynomial.C r * p).leadingCoeff = r
• 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.natDegree_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).natDegree = p.natDegree
• Polynomial.natDegree_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).natDegree = p.natDegree
• 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.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.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.leadingCoeff_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).leadingCoeff = a * p.leadingCoeff
• Polynomial.leadingCoeff_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).leadingCoeff = p.leadingCoeff * a
• 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_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.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.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.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.natDegree_sub_C 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p : Polynomial R} {a : R} : (p - Polynomial.C a).natDegree = p.natDegree
• 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.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.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.isUnit_iff 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} : IsUnit p ↔ ∃ r, IsUnit r ∧ Polynomial.C r = p
• Polynomial.Monic.C_dvd_iff_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) {a : R} : Polynomial.C a ∣ p ↔ IsUnit a
• 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.algebraMap_eq 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] : algebraMap R (Polynomial R) = Polynomial.C
• Polynomial.CAlgHom_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : A) : Polynomial.CAlgHom a✝ = Polynomial.C a✝
• 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.algebraMap_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R (Polynomial A)) r = Polynomial.C ((algebraMap R A) r)
• 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
• Polynomial.C_eq_algebraMap 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (r : R) : Polynomial.C r = (algebraMap R (Polynomial R)) r
• Polynomial.aeval_C 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) : (Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
• Polynomial.aevalTower_C 📋 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') (x : R) : (Polynomial.aevalTower g y) (Polynomial.C x) = g x
• Polynomial.mapAlgHom_eq_eval₂AlgHom_CAlgHom 📋 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) : Polynomial.mapAlgHom f = Polynomial.eval₂AlgHom (Polynomial.CAlgHom.comp f) Polynomial.X ⋯
• Polynomial.aevalTower_comp_C 📋 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)).comp Polynomial.C = ↑g
• Polynomial.dvd_comp_X_add_C_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (Polynomial.X + Polynomial.C a) ↔ p.comp (Polynomial.X - Polynomial.C a) ∣ q
• Polynomial.dvd_comp_X_sub_C_iff 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (Polynomial.X - Polynomial.C a) ↔ p.comp (Polynomial.X + Polynomial.C a) ∣ q
• Polynomial.algEquivAevalXAddC_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) : (Polynomial.algEquivAevalXAddC t) a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a

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