Loogle!

Result

Found 373 declarations mentioning Polynomial.Monic. Of these, only the first 200 are shown.

• Polynomial.Monic 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (p : Polynomial R) : Prop
• Polynomial.monic_X 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.X.Monic
• Polynomial.Monic.decidable 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} [DecidableEq R] : Decidable p.Monic
• Polynomial.monic_one 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] : Polynomial.Monic 1
• Polynomial.Monic.ne_zero 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) : p ≠ 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.monic_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).Monic
• Polynomial.Monic.ne_zero_of_polynomial_ne 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p q r : Polynomial R} (hp : p.Monic) (hne : q ≠ r) : p ≠ 0
• Polynomial.Monic.ne_zero_of_ne 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (h : 0 ≠ 1) {p : Polynomial R} (hp : p.Monic) : p ≠ 0
• Polynomial.Monic.coeff_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.coeff p.natDegree = 1
• Polynomial.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.monic_of_subsingleton 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Subsingleton R] (p : Polynomial R) : p.Monic
• Polynomial.eq_one_of_monic_natDegree_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1
• Polynomial.Monic.natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (hf : p.Monic) : p.natDegree = 0 ↔ p = 1
• 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.Monic.natDegree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : 0 < p.natDegree ↔ p ≠ 1
• Polynomial.Monic.degree_mul 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) : (p * q).degree = p.degree + q.degree
• Polynomial.monic_of_natDegree_le_of_coeff_eq_one 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) : p.Monic
• Polynomial.Monic.degree_pos 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : 0 < p.degree ↔ p ≠ 1
• Polynomial.monic_of_degree_le 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (pn : p.degree ≤ ↑n) (p1 : p.coeff n = 1) : p.Monic
• Polynomial.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.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.Monic.natDegree_pos_of_not_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) : 0 < p.natDegree
• Polynomial.Monic.degree_pos_of_not_isUnit 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) : 0 < p.degree
• Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {a p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < a.natDegree
• Polynomial.degree_pos_of_not_isUnit_of_dvd_monic 📋 Mathlib.Algebra.Polynomial.Degree.Units
  {R : Type u} [CommSemiring R] {a p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < a.degree
• Polynomial.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.map_monic_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) [Nontrivial S] : Polynomial.map f p ≠ 0
• Polynomial.map_monic_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) : Polynomial.map f p = 0 ↔ ∀ (x : R), f x = 0
• Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h₁ : p.Monic) : p = Polynomial.X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree
• Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h₁ : p.Monic) : p = Polynomial.X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree
• 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.monic_zero_iff_subsingleton 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] : Polynomial.Monic 0 ↔ Subsingleton R
• Polynomial.not_monic_zero 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] [Nontrivial R] : ¬Polynomial.Monic 0
• Polynomial.MonicDegreeEq.mk 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {n : ℕ} [Semiring R] (p : Polynomial R) (hp : p.Monic) (hp' : p.natDegree = n) : Polynomial.MonicDegreeEq R n
• Polynomial.Monic.isRegular 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u_1} [Ring R] {p : Polynomial R} (hp : p.Monic) : IsRegular p
• Polynomial.Monic.map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hp : p.Monic) : (Polynomial.map f p).Monic
• Polynomial.eq_of_monic_of_associated 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hpq : Associated p q) : p = q
• Polynomial.Monic.comp 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic
• Polynomial.monic_zero_iff_subsingleton' 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] : Polynomial.Monic 0 ↔ (∀ (f g : Polynomial R), f = g) ∧ ∀ (a b : R), a = b
• Polynomial.Monic.eq_one_of_isUnit 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hpu : IsUnit p) : p = 1
• Polynomial.Monic.mul 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).Monic
• Polynomial.Monic.of_mul_monic_left 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic
• Polynomial.Monic.of_mul_monic_right 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic
• Polynomial.Monic.isUnit_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) : IsUnit p ↔ p = 1
• Polynomial.Monic.natDegree_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).natDegree = P.natDegree
• Polynomial.Monic.degree_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).degree = P.degree
• Polynomial.Monic.pow 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).Monic
• Polynomial.not_monic_zero_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] : ¬Polynomial.Monic 0 ↔ 0 ≠ 1
• Polynomial.Monic.add_of_left 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p + q).Monic
• Polynomial.Monic.add_of_right 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hq : q.Monic) (hpq : p.degree < q.degree) : (p + q).Monic
• Polynomial.Monic.degree_le_zero_iff_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1
• Polynomial.Monic.natDegree_mul 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).natDegree = p.natDegree + q.natDegree
• Polynomial.monic_multiset_prod_of_monic 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (ht : ∀ i ∈ t, (f i).Monic) : (Multiset.map f t).prod.Monic
• Polynomial.monic_prod_of_monic 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (hs : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).Monic
• Polynomial.monic_of_injective 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} (hp : (Polynomial.map f p).Monic) : p.Monic
• Polynomial.Monic.natDegree_pow 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree
• Function.Injective.monic_map_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} : p.Monic ↔ (Polynomial.map f p).Monic
• Polynomial.Monic.natDegree_mul_comm 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) : (p * q).natDegree = (q * p).natDegree
• Polynomial.monic_finprod_of_monic 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] (α : Type u_1) (f : α → Polynomial R) (hf : ∀ i ∈ Function.mulSupport f, (f i).Monic) : (finprod f).Monic
• Polynomial.Monic.degree_mul_comm 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (q : Polynomial R) : (p * q).degree = (q * p).degree
• Polynomial.Monic.nextCoeff_mul 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) : (p * q).nextCoeff = p.nextCoeff + q.nextCoeff
• Polynomial.Monic.eq_one_of_map_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic) (map_eq : Polynomial.map f p = 1) : p = 1
• Polynomial.Monic.mul_left_ne_zero 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) {q : Polynomial R} (hq : q ≠ 0) : q * p ≠ 0
• Polynomial.Monic.mul_right_ne_zero 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) {q : Polynomial R} (hq : q ≠ 0) : p * q ≠ 0
• Polynomial.Monic.mul_left_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : q * p = 0 ↔ q = 0
• Polynomial.Monic.mul_right_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : p * q = 0 ↔ q = 0
• Polynomial.Monic.natDegree_le_of_dvd 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q ≠ 0) (hdvd : p ∣ q) : p.natDegree ≤ q.natDegree
• Polynomial.monic_X_add_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] (x : R) : (Polynomial.X + Polynomial.C x).Monic
• Polynomial.Monic.not_dvd_of_natDegree_lt 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) : ¬p ∣ q
• Polynomial.Monic.natDegree_mul' 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree
• Polynomial.Monic.nextCoeff_pow 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff
• Polynomial.Monic.sub_of_left 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p q : Polynomial R} (hp : p.Monic) (hpq : q.degree < p.degree) : (p - q).Monic
• Polynomial.Monic.not_dvd_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q
• Polynomial.Monic.nextCoeff_prod 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).nextCoeff = ∑ i ∈ s, (f i).nextCoeff
• Polynomial.Monic.comp_X_add_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X + Polynomial.C r)).Monic
• Polynomial.Monic.mul_natDegree_lt_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {q : Polynomial R} : (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
• Polynomial.Monic.nextCoeff_multiset_prod 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (h : ∀ i ∈ t, (f i).Monic) : (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
• Polynomial.monic_X_pow_add 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (Polynomial.X ^ n + p).Monic
• Polynomial.monic_X_sub_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] (x : R) : (Polynomial.X - Polynomial.C x).Monic
• 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.MonicDegreeEq.monic 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {n : ℕ} [Semiring R] (p : Polynomial.MonicDegreeEq R n) : (↑p).Monic
• Polynomial.monic_X_pow_add_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} (a : R) [Semiring R] {n : ℕ} (h : n ≠ 0) : (Polynomial.X ^ n + Polynomial.C a).Monic
• Polynomial.monic_X_pow_sub 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} (H : p.degree < ↑n) : (Polynomial.X ^ n - p).Monic
• Polynomial.Monic.comp_X_sub_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X - Polynomial.C r)).Monic
• Polynomial.MonicDegreeEq.mk_coe 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {n : ℕ} [Semiring R] (p : Polynomial R) (hp : p.Monic) (hp' : p.natDegree = n) : ↑(Polynomial.MonicDegreeEq.mk p hp hp') = p
• Polynomial.monic_X_pow_sub_C 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (Polynomial.X ^ n - Polynomial.C a).Monic
• Polynomial.Monic.irreducible_iff_natDegree 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
• Polynomial.Monic.irreducible_iff_lt_natDegree_lt 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
• Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 2) : ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
• Polynomial.Monic.irreducible_iff_natDegree' 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Finset.Ioc 0 (p.natDegree / 2)
• Polynomial.irreducible_of_monic 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
• Polynomial.Monic.as_sum 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p = Polynomial.X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.natDegree_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
• Polynomial.degree_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} {ι : Type w} (s : Finset ι) [CommSemiring R] (f : ι → Polynomial R) [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
• Polynomial.natDegree_multiset_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) (h : ∀ f ∈ t, f.Monic) : t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
• Polynomial.degree_multiset_prod_of_monic 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommSemiring R] (t : Multiset (Polynomial R)) [Nontrivial R] (h : ∀ f ∈ t, f.Monic) : t.prod.degree = (Multiset.map Polynomial.degree t).sum
• Polynomial.monic_geom_sum_X 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, Polynomial.X ^ i).Monic
• Polynomial.Monic.geom_sum 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic
• Polynomial.Monic.geom_sum' 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic
• Polynomial.monicEquivDegreeLT 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : { p // p.Monic ∧ p.natDegree = n } ≃ ↥(Polynomial.degreeLT R n)
• Polynomial.monic_restriction 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Ring R] {p : Polynomial R} : p.restriction.Monic ↔ p.Monic
• Polynomial.divModByMonicAux 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (_p : Polynomial R) {q : Polynomial R} : q.Monic → Polynomial R × Polynomial R
• Polynomial.modByMonic_eq_of_not_monic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) : p %ₘ q = p
• Polynomial.natDegree_modByMonic_le 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) : (p %ₘ g).natDegree ≤ g.natDegree
• Polynomial.modByMonic_self 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p : Polynomial R} (hp : p.Monic) : p %ₘ p = 0
• Polynomial.degree_modByMonic_le 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) : (p %ₘ q).degree ≤ q.degree
• Polynomial.degree_modByMonic_lt 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] [Nontrivial R] (p : Polynomial R) {q : Polynomial R} (_hq : q.Monic) : (p %ₘ q).degree < q.degree
• Polynomial.divByMonic_eq_of_not_monic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) : p /ₘ q = 0
• Polynomial.natDegree_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (f : Polynomial R) {g : Polynomial R} (hg : g.Monic) : (f /ₘ g).natDegree = f.natDegree - g.natDegree
• Polynomial.modByMonic_eq_self_iff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) : p %ₘ q = p ↔ p.degree < q.degree
• Polynomial.eq_of_monic_of_dvd_of_natDegree_le 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hdvd : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) : q = p
• Polynomial.mul_divByMonic_cancel_left 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmo : q.Monic) : q * p /ₘ q = p
• Polynomial.natDegree_modByMonic_lt 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmq : q.Monic) (hq : q ≠ 1) : (p %ₘ q).natDegree < q.natDegree
• Polynomial.finiteMultiplicity_of_degree_pos_of_monic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Semiring R] {p q : Polynomial R} (hp : 0 < p.degree) (hmp : p.Monic) (hq : q ≠ 0) : FiniteMultiplicity p q
• Polynomial.divByMonic_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) : p /ₘ q = 0 ↔ p.degree < q.degree
• 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.self_mul_modByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) : q * p %ₘ q = 0
• Polynomial.degree_add_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) (h : q.degree ≤ p.degree) : q.degree + (p /ₘ q).degree = p.degree
• Polynomial.map_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q
• Polynomial.map_modByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
• Polynomial.modByMonic_eq_zero_iff_dvd 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) : p %ₘ q = 0 ↔ q ∣ p
• Polynomial.mul_self_modByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p q : Polynomial R} (hq : q.Monic) : p * q %ₘ q = 0
• 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.map_mod_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q ∧ Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
• Polynomial.div_modByMonic_unique 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {f g : Polynomial R} (q r : Polynomial R) (hg : g.Monic) (h : r + g * q = f ∧ r.degree < g.degree) : f /ₘ g = q ∧ f %ₘ g = r
• Polynomial.modByMonic_eq_of_dvd_sub 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [CommRing R] {p₁ p₂ q : Polynomial R} (hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q
• Polynomial.map_dvd_map 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Injective ⇑f) {x y : Polynomial R} (hx : x.Monic) : Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
• 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.sum_modByMonic_coeff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ ↑n) : ∑ i, (Polynomial.monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
• 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.Monic.prime_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) : Prime p
• Polynomial.Monic.irreducible_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) : Irreducible p
• Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [Nontrivial R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : p.Monic) {x : S} (hx : (Polynomial.aeval x) p = 0) : 0 < p.natDegree
• Polynomial.Monic.mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} (h : p.Monic) : p ∈ nonZeroDivisors (Polynomial R)
• Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {p : Polynomial R} (hp : p.Monic) : ((-1) ^ p.natDegree * p.comp (-Polynomial.X)).Monic
• Polynomial.mem_ker_divByMonic 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {q : Polynomial R} [Nontrivial R] (hq : q.Monic) {p : Polynomial R} : p ∈ q.divByMonicHom.ker ↔ p.degree < q.degree
• Polynomial.mem_ker_modByMonic 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) {p : Polynomial R} : p ∈ q.modByMonicHom.ker ↔ q ∣ p
• Polynomial.Monic.expand 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : f.Monic → ((Polynomial.expand R p) f).Monic
• Polynomial.monic_expand_iff 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : ((Polynomial.expand R p) f).Monic ↔ f.Monic
• 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.Monic.roots_map_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} (hm : p.Monic) (f : A →+* B) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.monic_finprod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] {α : Type u_1} (b : α → R) : (∏ᶠ (k : α), (Polynomial.X - Polynomial.C (b k))).Monic
• Polynomial.monic_prod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] {α : Type u_1} (b : α → R) (s : Finset α) : (∏ a ∈ s, (Polynomial.X - Polynomial.C (b a))).Monic
• Polynomial.monic_multisetProd_X_sub_C 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] (s : Multiset R) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod.Monic
• Polynomial.Monic.mem_rootSet 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} (hp : p.Monic) {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] {a : S} : a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
• Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p.Monic) (hroots : p.roots.card = p.natDegree) : (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
• Polynomial.Monic.irreducible_iff_degree_lt 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (p_monic : p.Monic) (p_1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
• Polynomial.monic_map_iff 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).Monic ↔ p.Monic
• Polynomial.Monic.normalize_eq_self 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [NormalizationMonoid R] {p : Polynomial R} (hp : p.Monic) : normalize p = p
• Polynomial.divByMonic_eq_div 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : q.Monic) : p /ₘ q = p / q
• Polynomial.modByMonic_eq_mod 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : q.Monic) : p %ₘ q = p % q
• Polynomial.monic_normalize 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp0 : p ≠ 0) : (normalize p).Monic
• Polynomial.normalize_eq_self_iff_monic 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] [DecidableEq R] {p : Polynomial R} (hp : p ≠ 0) : normalize p = p ↔ p.Monic
• Polynomial.monic_mapAlg_iff 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Field R] [Semiring S] [Nontrivial S] [Algebra R S] {p : Polynomial R} : ((Polynomial.mapAlg R S) p).Monic ↔ p.Monic
• Polynomial.irreducible_iff_lt_natDegree_lt 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p : Polynomial R} (hp0 : p ≠ 0) (hpu : ¬IsUnit p) : Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
• Polynomial.mem_normalizedFactors_iff 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [Field R] {p q : Polynomial R} [DecidableEq R] (hq : q ≠ 0) : p ∈ UniqueFactorizationMonoid.normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
• Polynomial.Monic.isPrimitive 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : p.IsPrimitive
• Polynomial.fintypeSubtypeMonicDvd 📋 Mathlib.RingTheory.Polynomial.UniqueFactorization
  {D : Type u} [CommRing D] [UniqueFactorizationMonoid D] (f : Polynomial D) (hf : f ≠ 0) : Fintype { g // g.Monic ∧ g ∣ f }
• Polynomial.exists_monic_irreducible_factor 📋 Mathlib.RingTheory.Polynomial.UniqueFactorization
  {F : Type u_1} [Field F] (f : Polynomial F) (hu : ¬IsUnit f) : ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
• Matrix.det_matrixOfPolynomials 📋 Mathlib.LinearAlgebra.Matrix.Block
  {R : Type v} [CommRing R] {n : ℕ} (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i) (h_monic : ∀ (i : Fin n), (p i).Monic) : (Matrix.of fun i j => (p j).coeff ↑i).det = 1
• Matrix.charpoly_monic 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
  {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : M.charpoly.Monic
• LinearMap.exists_monic_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) : ∃ p, p.Monic ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
• IsIntegral.of_aeval_monic 📋 Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {p : Polynomial R} (monic : p.Monic) (deg : p.natDegree ≠ 0) (hx : IsIntegral R ((Polynomial.aeval x) p)) : IsIntegral R x
• Submodule.span_range_natDegree_eq_adjoin 📋 Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  {R : Type u_6} {A : Type u_7} [CommRing R] [Semiring A] [Algebra R A] {x : A} {f : Polynomial R} (hf : f.Monic) (hfx : (Polynomial.aeval x) f = 0) : Submodule.span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule R[x]
• Polynomial.lifts_and_natDegree_eq_and_monic 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) (hp : p.Monic) : ∃ q, Polynomial.map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
• Polynomial.lifts_and_degree_eq_and_monic 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} [Nontrivial S] {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) (hp : p.Monic) : ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic
• Polynomial.monic_of_monic_mapAlg 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : ((Polynomial.mapAlg R S) p).Monic) : p.Monic
• Polynomial.splits_of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.splits_of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.comp_of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum
• Polynomial.Splits.eval_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) (x : R) : Polynomial.eval x f = (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.map_sub_sprod_roots_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod
• Polynomial.map_sub_roots_sprod_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (g.roots ×ˢ s)).prod = (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.Splits.eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.mem_lift_of_roots_mem_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) {S : Type u_4} [Ring S] (i : S →+* R) (hr : ∀ a ∈ f.roots, a ∈ i.range) : f ∈ Polynomial.lifts i
• Polynomial.Splits.aeval_eq_prod_aroots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] (hf : (Polynomial.map (algebraMap R A) f).Splits) (hm : f.Monic) (x : A) : (Polynomial.aeval x) f = (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
• Polynomial.Splits.eval_root_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : Polynomial.eval x (Polynomial.derivative f) = (Multiset.map (fun x_1 => x - x_1) (f.roots.erase x)).prod
• Polynomial.monic_scaleRoots_iff 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] {p : Polynomial R} (s : R) : (p.scaleRoots s).Monic ↔ p.Monic
• Polynomial.monic_integralNormalization 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.integralNormalization.Monic
• Polynomial.monic_toSubring 📋 Mathlib.RingTheory.Polynomial.Subring
  {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).Monic ↔ p.Monic
• roots_mem_integralClosure 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) : a ∈ integralClosure R S
• Polynomial.Monic.quotient_isIntegral 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {S : Type u_4} [CommRing S] {g : Polynomial S} (mon : g.Monic) {I : Ideal (Polynomial S)} (h : g ∈ I) : ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S (Polynomial S))).IsIntegral
• Polynomial.Monic.quotient_isIntegralElem 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {S : Type u_4} [CommRing S] {g : Polynomial S} (mon : g.Monic) {I : Ideal (Polynomial S)} (h : g ∈ I) : ((Ideal.Quotient.mk I).comp (algebraMap S (Polynomial S))).IsIntegralElem ((Ideal.Quotient.mk I) Polynomial.X)
• Polynomial.div_eq_quo_add_rem_div 📋 Mathlib.RingTheory.IntegralDomain
  {R : Type u_1} [CommRing R] [IsDomain R] (K : Type u_3) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g : Polynomial R} (hg : g.Monic) : ∃ q r, r.degree < g.degree ∧ (algebraMap (Polynomial R) K) f / (algebraMap (Polynomial R) K) g = (algebraMap (Polynomial R) K) q + (algebraMap (Polynomial R) K) r / (algebraMap (Polynomial R) K) g
• Cubic.monic_of_d_eq_one' 📋 Mathlib.Algebra.CubicDiscriminant
  : { a := 0, b := 0, c := 0, d := 1 }.toPoly.Monic
• Cubic.monic_of_a_eq_one 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {P : Cubic R} [Semiring R] (ha : P.a = 1) : P.toPoly.Monic

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