Loogle!

Result

Found 308 declarations mentioning Polynomial.leadingCoeff. Of these, only the first 200 are shown.

• Polynomial.leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) : R
• Polynomial.leadingCoeff_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.leadingCoeff = 1
• Polynomial.leadingCoeff_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.leadingCoeff 0 = 0
• Polynomial.Monic.leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.leadingCoeff = 1
• Polynomial.Monic.def 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.Monic ↔ p.leadingCoeff = 1
• Polynomial.leadingCoeff_one 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.leadingCoeff 1 = 1
• Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff = 0 ↔ p.degree = ⊥
• Polynomial.coeff_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeff p.natDegree = p.leadingCoeff
• Polynomial.leadingCoeff_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff = 0 ↔ p = 0
• Polynomial.leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} : p.leadingCoeff ≠ 0 ↔ p ≠ 0
• Polynomial.leadingCoeff_neg 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] (p : Polynomial R) : (-p).leadingCoeff = -p.leadingCoeff
• Polynomial.leadingCoeff_C 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).leadingCoeff = a
• 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.leadingCoeff_monomial 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : ((Polynomial.monomial n) a).leadingCoeff = a
• 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.degree_sub_lt 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < p.degree
• Polynomial.degree_sub_lt_left 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hp0 : p ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < p.degree
• Polynomial.degree_sub_lt_right 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} (hd : p.degree = q.degree) (hq0 : q ≠ 0) (hlc : p.leadingCoeff = q.leadingCoeff) : (p - q).degree < q.degree
• Polynomial.leadingCoeff_mul_X 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} : (p * Polynomial.X).leadingCoeff = p.leadingCoeff
• Polynomial.leadingCoeff_monic_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) : (p * q).leadingCoeff = q.leadingCoeff
• Polynomial.leadingCoeff_mul_monic 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) : (p * q).leadingCoeff = p.leadingCoeff
• Polynomial.leadingCoeff_add_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p + q).leadingCoeff = q.leadingCoeff
• Polynomial.leadingCoeff_add_of_degree_lt' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p + q).leadingCoeff = p.leadingCoeff
• Polynomial.leadingCoeff_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] (p q : Polynomial R) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
• Polynomial.leadingCoeff_dvd_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] {a p : Polynomial R} (hap : a ∣ p) : a.leadingCoeff ∣ p.leadingCoeff
• 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.leadingCoeff_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ) : (p ^ n).leadingCoeff = p.leadingCoeff ^ n
• Polynomial.leadingCoeff_sub_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree < p.degree) : (p - q).leadingCoeff = p.leadingCoeff
• Polynomial.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_mul' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree
• 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.leadingCoeff_mul' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
• Polynomial.natDegree_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.leadingCoeff ^ n ≠ 0) : (p ^ n).natDegree = n * p.natDegree
• Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).degree = max p.degree q.degree
• Polynomial.degree_mul' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).degree = p.degree + q.degree
• Polynomial.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.degree_smul_of_isRightRegular_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (ha : a ≠ 0) (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree
• Polynomial.leadingCoeff_sub_of_degree_lt' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree < q.degree) : (p - q).leadingCoeff = -q.leadingCoeff
• Polynomial.leadingCoeffHom_apply 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) : Polynomial.leadingCoeffHom p = p.leadingCoeff
• 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.leadingCoeff_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
• 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.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.leadingCoeff_add_of_degree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff + q.leadingCoeff ≠ 0) : (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
• Polynomial.degree_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : p.leadingCoeff ^ n ≠ 0 → (p ^ n).degree = n • p.degree
• Polynomial.leadingCoeff_sub_of_degree_eq 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Ring R] {p q : Polynomial R} (h : p.degree = q.degree) (hlc : p.leadingCoeff ≠ q.leadingCoeff) : (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
• Polynomial.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.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.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.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.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.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.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_map_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map_eq_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).degree = p.degree
• Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit f.leadingCoeff) (H : IsUnit (Polynomial.map φ f)) : IsUnit f
• Polynomial.natDegree_map_lt' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : 0 < p.natDegree) : (Polynomial.map f p).natDegree < p.natDegree
• Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.nextCoeff_map_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).nextCoeff = f p.nextCoeff
• Polynomial.degree_map_lt 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (Polynomial.map f p).degree < p.degree
• Polynomial.natDegree_map_lt 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : Polynomial.map f p ≠ 0) : (Polynomial.map f p).natDegree < p.natDegree
• 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.natDegree_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).degree = p.degree
• Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).nextCoeff = f p.nextCoeff
• Polynomial.leadingCoeff_comp 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} [NoZeroDivisors R] (hq : q.natDegree ≠ 0) : (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
• Polynomial.leadingCoeff_map_of_injective 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.natDegree_comp_eq_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) : (p.comp q).natDegree = p.natDegree * q.natDegree
• Polynomial.natDegree_map_eq_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
• Polynomial.degree_map_eq_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
• Polynomial.natDegree_C_mul_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) : (Polynomial.C a * p).natDegree = p.natDegree
• Polynomial.natDegree_mul_C_eq_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : p.leadingCoeff * a ≠ 0) : (p * Polynomial.C a).natDegree = p.natDegree
• Polynomial.comp_neg_X_leadingCoeff_eq 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} [Ring R] (p : Polynomial R) : (p.comp (-Polynomial.X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff
• Polynomial.degree_C_mul_of_mul_ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff ≠ 0) : (Polynomial.C a * p).degree = p.degree
• Polynomial.degree_add_degree_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) : p.degree + (Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
• Polynomial.degree_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] {p : Polynomial K} (hp0 : p ≠ 0) : (Polynomial.C p.leadingCoeff⁻¹).degree = 0
• Polynomial.natDegree_mul_leadingCoeff_self_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) : (p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree
• Polynomial.degree_mul_leadingCoeff_self_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) : (p * Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
• Polynomial.monic_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] {p : Polynomial K} (h : p ≠ 0) : (p * Polynomial.C p.leadingCoeff⁻¹).Monic
• Polynomial.irreducible_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] {p : Polynomial K} : Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) ↔ Irreducible p
• Polynomial.natDegree_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) : (p * Polynomial.C q.leadingCoeff⁻¹).natDegree = p.natDegree
• Polynomial.degree_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q ≠ 0) : (p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
• Polynomial.dvd_mul_leadingCoeff_inv 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {K : Type u_1} [DivisionRing K] {p q : Polynomial K} (hp0 : p ≠ 0) : q ∣ p * Polynomial.C p.leadingCoeff⁻¹ ↔ q ∣ p
• Polynomial.monomial_natDegree_leadingCoeff_eq_self 📋 Mathlib.Algebra.Polynomial.Degree.Monomial
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : (Polynomial.monomial p.natDegree) p.leadingCoeff = p
• Polynomial.C_mul_X_pow_eq_self 📋 Mathlib.Algebra.Polynomial.Degree.Monomial
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
• Polynomial.leadingCoeff_eraseLead_eq_nextCoeff 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff ≠ 0) : f.eraseLead.leadingCoeff = f.nextCoeff
• Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.eraseLead + (Polynomial.monomial f.natDegree) f.leadingCoeff = f
• Polynomial.eraseLead_add_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.eraseLead + Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f
• Polynomial.self_sub_monomial_natDegree_leadingCoeff 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_2} [Ring R] (f : Polynomial R) : f - (Polynomial.monomial f.natDegree) f.leadingCoeff = f.eraseLead
• Polynomial.self_sub_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_2} [Ring R] (f : Polynomial R) : f - Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f.eraseLead
• Polynomial.reverse_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.reverse.leadingCoeff = f.trailingCoeff
• Polynomial.reverse_trailingCoeff 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.reverse.trailingCoeff = f.leadingCoeff
• Polynomial.coeff_zero_reverse 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.reverse.coeff 0 = f.leadingCoeff
• Polynomial.reverse_mul 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {f g : Polynomial R} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) : (f * g).reverse = f.reverse * g.reverse
• Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} : q * p = 0 ↔ q = 0
• Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {q : Polynomial R} : p * q = 0 ↔ q = 0
• Polynomial.leadingCoeff_smul_of_smul_regular 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff
• Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : b * p.leadingCoeff = 1) : (Polynomial.C b * p).Monic
• Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : p.leadingCoeff * b = 1) : (p * Polynomial.C b).Monic
• Polynomial.Monic.sub_of_right 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.leadingCoeff = -1) (hpq : p.degree < q.degree) : (p - q).Monic
• Polynomial.monic_of_isUnit_leadingCoeff_inv_smul 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) : (h.unit⁻¹ • p).Monic
• Polynomial.leadingCoeff_prod 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R) : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
• Polynomial.leadingCoeff_multiset_prod 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) : t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod
• Polynomial.natDegree_prod' 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
• Polynomial.leadingCoeff_multiset_prod' 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : (Multiset.map Polynomial.leadingCoeff t).prod ≠ 0) : t.prod.leadingCoeff = (Multiset.map Polynomial.leadingCoeff t).prod
• Polynomial.leadingCoeff_prod' 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0) : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
• Polynomial.natDegree_multiset_prod' 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : (Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0) : t.prod.natDegree = (Multiset.map (fun f => f.natDegree) t).sum
• Polynomial.leadingCoeff_sum_of_degree_eq 📋 Mathlib.Algebra.Polynomial.BigOperators
  {ι : Type w} {S : Type u_1} [Semiring S] {f : ι → Polynomial S} {s : Finset ι} {d : WithBot ℕ} (hd : ∀ k ∈ s, (f k).degree = d) (hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0) : (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff
• Ideal.mem_leadingCoeff 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
• Ideal.mem_leadingCoeffNth 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (n : ℕ) (x : R) : x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
• Polynomial.leadingCoeff_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] [IsAddTorsionFree R] (p : Polynomial R) : (Polynomial.derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree
• Polynomial.leadingCoeff_divByMonic_of_monic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p q : Polynomial R} (hmonic : q.Monic) (hdegree : q.degree ≤ p.degree) : (p /ₘ q).leadingCoeff = p.leadingCoeff
• Polynomial.eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hdvd : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) : q = p * Polynomial.C q.leadingCoeff
• Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) : p = q
• Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (hpq : p ∣ q) (h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) : Associated p q
• Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.Monic) (hdvd : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) : q = Polynomial.C q.leadingCoeff * p
• Polynomial.leadingCoeff_divByMonic_X_sub_C 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (hp : p.degree ≠ 0) (a : R) : (p /ₘ (Polynomial.X - Polynomial.C a)).leadingCoeff = p.leadingCoeff
• Polynomial.div_wf_lemma 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree ≤ p.degree ∧ p ≠ 0) (hq : q.Monic) : (p - q * (Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree))).degree < p.degree
• Polynomial.mem_nonZeroDivisors_of_leadingCoeff 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} (h : p.leadingCoeff ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)
• Polynomial.leadingCoeff_expand 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : ((Polynomial.expand R p) f).leadingCoeff = f.leadingCoeff
• Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm 📋 Mathlib.Algebra.Polynomial.CancelLeads
  {R : Type u_1} [Ring R] {p q : Polynomial R} (comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff) (h : p.natDegree ≤ q.natDegree) (hq : 0 < q.natDegree) : (p.cancelLeads q).natDegree < q.natDegree
• Polynomial.Monic.isUnit_leadingCoeff_of_dvd 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {a p : Polynomial R} (hp : p.Monic) (hap : a ∣ p) : IsUnit a.leadingCoeff
• Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : p.roots.card = p.natDegree) : Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
• Polynomial.leadingCoeff_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.leadingCoeff_normalize 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [NormalizationMonoid R] (p : Polynomial R) : (normalize p).leadingCoeff = normalize p.leadingCoeff
• Polynomial.leadingCoeff_div 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p q : Polynomial R} (hpq : q.degree ≤ p.degree) : (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
• Polynomial.coe_normUnit 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [NormalizationMonoid R] {p : Polynomial R} : ↑(normUnit p) = Polynomial.C ↑(normUnit p.leadingCoeff)
• Polynomial.mod_def 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p q : Polynomial R} : p % q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
• Polynomial.coe_normUnit_of_ne_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp : p ≠ 0) : ↑(normUnit p) = Polynomial.C p.leadingCoeff⁻¹
• Polynomial.leadingCoeff_mul_prod_normalizedFactors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] [DecidableEq R] (a : Polynomial R) : Polynomial.C a.leadingCoeff * (UniqueFactorizationMonoid.normalizedFactors a).prod = a
• Polynomial.div_def 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p q : Polynomial R} : p / q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
• Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.content = gcd p.leadingCoeff p.eraseLead.content
• Polynomial.content_mul_aux 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} : gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff
• Polynomial.transcendental 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} [CommRing R] (f : Polynomial R) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) : Transcendental R f
• IsAlgebraic.of_aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (f : Polynomial R) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) (H : IsAlgebraic R ((Polynomial.aeval r) f)) : IsAlgebraic R r
• Transcendental.aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (H : Transcendental R r) (f : Polynomial R) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) : Transcendental R ((Polynomial.aeval r) f)
• Polynomial.leadingCoeff_det_X_one_add_C 📋 Mathlib.LinearAlgebra.Matrix.Polynomial
  {n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : (Polynomial.X • 1 + A.map ⇑Polynomial.C).det.leadingCoeff = 1
• Polynomial.hasseDeriv_natDegree_eq_C 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.hasseDeriv f.natDegree) f = Polynomial.C f.leadingCoeff
• Polynomial.leadingCoeff_taylor 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((Polynomial.taylor r) f).leadingCoeff = f.leadingCoeff
• Polynomial.coeff_taylor_natDegree 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((Polynomial.taylor r) f).coeff f.natDegree = f.leadingCoeff
• Polynomial.splits_of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.splits_of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.comp_of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.nextCoeff = -f.leadingCoeff * f.roots.sum
• Polynomial.Splits.eval_eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (x : R) : Polynomial.eval x f = f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod
• Polynomial.splits_iff_exists_multiset' 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} : f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X + Polynomial.C x) m).prod
• Polynomial.Splits.eq_X_sub_C_of_single_root 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) {x : R} (hr : f.roots = {x}) : f = Polynomial.C f.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Polynomial.splits_iff_exists_multiset 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} : f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) m).prod
• Polynomial.Splits.eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.aeval_eq_prod_aroots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R S) f).Splits) (x : S) : (Polynomial.aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots S)).prod
• Polynomial.Splits.eval_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : Polynomial.eval x (Polynomial.derivative f) = f.leadingCoeff * (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
• Polynomial.leadingCoeff_scaleRoots 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] (p : Polynomial R) (r : R) : (p.scaleRoots r).leadingCoeff = p.leadingCoeff
• Polynomial.coeff_scaleRoots_natDegree 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) : (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
• Polynomial.map_scaleRoots 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (p : Polynomial R) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) : Polynomial.map f (p.scaleRoots x) = (Polynomial.map f p).scaleRoots (f x)
• Polynomial.scaleRoots_zero 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] (p : Polynomial R) : p.scaleRoots 0 = p.leadingCoeff • Polynomial.X ^ p.natDegree
• Polynomial.mul_scaleRoots' 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [CommSemiring R] (p q : Polynomial R) (r : R) (h : p.leadingCoeff * q.leadingCoeff ≠ 0) : (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
• Polynomial.pow_scaleRoots' 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [CommSemiring R] (p : Polynomial R) (r : R) (n : ℕ) (hp : p.leadingCoeff ^ n ≠ 0) : (p ^ n).scaleRoots r = p.scaleRoots r ^ n
• Polynomial.leadingCoeff_smul_integralNormalization 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {S : Type v} [CommSemiring S] (p : Polynomial S) : p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
• Polynomial.integralNormalization_map 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] (f : R →+* A) (p : Polynomial R) (H : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).integralNormalization = Polynomial.map f p.integralNormalization
• Polynomial.integralNormalization_mul_C_leadingCoeff 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] (p : Polynomial R) : p.integralNormalization * Polynomial.C p.leadingCoeff = p.scaleRoots p.leadingCoeff
• Polynomial.integralNormalization_coeff_ne_natDegree 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : i ≠ p.natDegree) : p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
• Polynomial.integralNormalization_coeff_degree_ne 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : p.degree ≠ ↑i) : p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
• Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} (i : ℕ) (hp : 1 ≤ p.natDegree) : p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
• Polynomial.integralNormalization_coeff 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} : p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
• Polynomial.integralNormalization_eval₂_eq_zero 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] {p : Polynomial R} (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
• Polynomial.integralNormalization_eval₂_leadingCoeff_mul 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) : Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
• Polynomial.integralNormalization_eval₂_eq_zero_of_commute 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] {p : Polynomial R} (f : R →+* A) {z : A} (hz : Polynomial.eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) (inj : ∀ (x : R), f x = 0 → x = 0) : Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
• Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} {A : Type u_1} [Semiring A] (h : 1 ≤ p.natDegree) (f : R →+* A) (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) : Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
• Polynomial.integralNormalization_aeval_smul 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {S : Type v} [CommSemiring S] {R : Type u_2} [CommSemiring R] [Algebra R S] {p : Polynomial R} (h : 1 ≤ p.natDegree) (x : S) : (Polynomial.aeval (p.leadingCoeff • x)) p.integralNormalization = p.leadingCoeff ^ (p.natDegree - 1) • (Polynomial.aeval x) p
• Polynomial.integralNormalization_aeval_eq_zero 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {S : Type v} {A : Type u_1} [CommSemiring S] [Semiring A] [Algebra S A] {f : Polynomial S} {z : A} (hz : (Polynomial.aeval z) f = 0) (inj : ∀ (x : S), (algebraMap S A) x = 0 → x = 0) : (Polynomial.aeval ((algebraMap S A) f.leadingCoeff * z)) f.integralNormalization = 0
• RingHom.isIntegralElem_leadingCoeff_mul 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (p : Polynomial R) (x : S) (h : Polynomial.eval₂ f x p = 0) : f.IsIntegralElem (f p.leadingCoeff * x)
• isIntegral_leadingCoeff_smul 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (p : Polynomial R) (x : S) [Algebra R S] (h : (Polynomial.aeval x) p = 0) : IsIntegral R (p.leadingCoeff • x)
• IsLocalization.scaleRoots_commonDenom_mem_lifts 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] (M : Submonoid R) {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] (p : Polynomial Rₘ) (hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range) : p.scaleRoots ((algebraMap R Rₘ) ↑(IsLocalization.commonDenom M p.support ⇑p.coeff)) ∈ Polynomial.lifts (algebraMap R Rₘ)
• RingHom.isIntegralElem_localization_at_leadingCoeff 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_5} {S : Type u_6} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hf : Polynomial.eval₂ f x p = 0) (M : Submonoid R) (hM : p.leadingCoeff ∈ M) {Rₘ : Type u_7} {Sₘ : Type u_8} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Submonoid.map f M) Sₘ] : (IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
• is_integral_localization_at_leadingCoeff 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {x : S} (p : Polynomial R) (hp : (Polynomial.aeval x) p = 0) (hM : p.leadingCoeff ∈ M) : (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
• Cubic.leadingCoeff_of_a_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a ≠ 0) : P.toPoly.leadingCoeff = P.a
• Cubic.leadingCoeff_of_a_ne_zero' 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {a b c d : R} [Semiring R] (ha : a ≠ 0) : { a := a, b := b, c := c, d := d }.toPoly.leadingCoeff = a
• Cubic.leadingCoeff_of_b_ne_zero' 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {b c d : R} [Semiring R] (hb : b ≠ 0) : { a := 0, b := b, c := c, d := d }.toPoly.leadingCoeff = b
• Cubic.leadingCoeff_of_c_eq_zero' 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {d : R} [Semiring R] : { a := 0, b := 0, c := 0, d := d }.toPoly.leadingCoeff = d
• Cubic.leadingCoeff_of_b_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b ≠ 0) : P.toPoly.leadingCoeff = P.b
• Cubic.leadingCoeff_of_c_ne_zero' 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {c d : R} [Semiring R] (hc : c ≠ 0) : { a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c
• Cubic.leadingCoeff_of_c_eq_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly.leadingCoeff = P.d
• Cubic.leadingCoeff_of_c_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : P.toPoly.leadingCoeff = P.c
• Polynomial.irreducible_of_eisenstein_criterion 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
  {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} {P : Ideal R} (hP : P.IsPrime) (hfl : f.leadingCoeff ∉ P) (hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) (hfd0 : 0 < f.degree) (h0 : f.coeff 0 ∉ P ^ 2) (hu : f.IsPrimitive) : Irreducible f
• Polynomial.generalizedEisenstein 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
  {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] {q f : Polynomial R} {p : ℕ} (hq_irr : Irreducible (Polynomial.map (algebraMap R K) q)) (hq_monic : q.Monic) (hf_prim : f.IsPrimitive) (hfd0 : 0 < f.natDegree) (hfP : (algebraMap R K) f.leadingCoeff ≠ 0) (hfmodP : Polynomial.map (algebraMap R K) f = Polynomial.C ((algebraMap R K) f.leadingCoeff) * Polynomial.map (algebraMap R K) q ^ p) (hfmodP2 : Polynomial.map (Ideal.Quotient.mk (RingHom.ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0) : Irreducible f
• Polynomial.IsEisensteinAt.leading 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R} (self : f.IsEisensteinAt 𝓟) : f.leadingCoeff ∉ 𝓟
• Polynomial.Monic.leadingCoeff_notMem 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : f.Monic) (h : 𝓟 ≠ ⊤) : f.leadingCoeff ∉ 𝓟
• Polynomial.IsEisensteinAt.mk 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R} (leading : f.leadingCoeff ∉ 𝓟) (mem : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) (notMem : f.coeff 0 ∉ 𝓟 ^ 2) : f.IsEisensteinAt 𝓟
• Polynomial.isEisensteinAt_iff 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R) : f.IsEisensteinAt 𝓟 ↔ f.leadingCoeff ∉ 𝓟 ∧ (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) ∧ f.coeff 0 ∉ 𝓟 ^ 2
• Polynomial.fwdDiff_iter_degree_eq_factorial 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] (P : Polynomial R) : ((fwdDiff 1)^[P.natDegree] fun x => Polynomial.eval x P) = P.leadingCoeff • ↑P.natDegree.factorial
• minpoly.Irreducible.eq_minpoly 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (hi : Irreducible p) (hx : (Polynomial.aeval x) p = 0) : p = Polynomial.C p.leadingCoeff * minpoly A x

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