Documentation

Mathlib.Data.Polynomial.Degree.Definitions

Theory of univariate polynomials #

The definitions include degree, Monic, leadingCoeff

Results include

degree p is the degree of the polynomial p, i.e. the largest X-exponent in p. degree p = some n when p ≠ 0 and n is the highest power of X that appears in p, otherwise degree 0 = ⊥.

Equations
Instances For
    Equations

    natDegree p forces degree p to ℕ, by defining natDegree 0 = 0.

    Equations
    Instances For
      def Polynomial.leadingCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
      R

      leadingCoeff p gives the coefficient of the highest power of X in p

      Equations
      Instances For
        def Polynomial.Monic {R : Type u} [Semiring R] (p : Polynomial R) :

        a polynomial is Monic if its leading coefficient is 1

        Equations
        Instances For
          Equations
          • Polynomial.Monic.decidable = id inferInstance
          @[simp]
          theorem Polynomial.degree_C {R : Type u} {a : R} [Semiring R] (ha : a 0) :
          Polynomial.degree (Polynomial.C a) = 0
          theorem Polynomial.degree_C_le {R : Type u} {a : R} [Semiring R] :
          Polynomial.degree (Polynomial.C a) 0
          theorem Polynomial.degree_C_lt {R : Type u} {a : R} [Semiring R] :
          Polynomial.degree (Polynomial.C a) < 1
          @[simp]
          theorem Polynomial.natDegree_C {R : Type u} [Semiring R] (a : R) :
          Polynomial.natDegree (Polynomial.C a) = 0
          @[simp]
          theorem Polynomial.degree_monomial {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
          @[simp]
          theorem Polynomial.degree_C_mul_X_pow {R : Type u} {a : R} [Semiring R] (n : ) (ha : a 0) :
          Polynomial.degree (Polynomial.C a * Polynomial.X ^ n) = n
          theorem Polynomial.degree_C_mul_X {R : Type u} {a : R} [Semiring R] (ha : a 0) :
          Polynomial.degree (Polynomial.C a * Polynomial.X) = 1
          theorem Polynomial.degree_C_mul_X_pow_le {R : Type u} [Semiring R] (n : ) (a : R) :
          Polynomial.degree (Polynomial.C a * Polynomial.X ^ n) n
          theorem Polynomial.degree_C_mul_X_le {R : Type u} [Semiring R] (a : R) :
          Polynomial.degree (Polynomial.C a * Polynomial.X) 1
          @[simp]
          theorem Polynomial.natDegree_C_mul_X_pow {R : Type u} [Semiring R] (n : ) (a : R) (ha : a 0) :
          Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ n) = n
          @[simp]
          theorem Polynomial.natDegree_C_mul_X {R : Type u} [Semiring R] (a : R) (ha : a 0) :
          Polynomial.natDegree (Polynomial.C a * Polynomial.X) = 1
          @[simp]
          theorem Polynomial.natDegree_monomial {R : Type u} [Semiring R] [DecidableEq R] (i : ) (r : R) :
          Polynomial.natDegree ((Polynomial.monomial i) r) = if r = 0 then 0 else i
          theorem Polynomial.ext_iff_natDegree_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : } (hp : Polynomial.natDegree p n) (hq : Polynomial.natDegree q n) :
          p = q in, Polynomial.coeff p i = Polynomial.coeff q i
          theorem Polynomial.ext_iff_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : } (hp : Polynomial.degree p n) (hq : Polynomial.degree q n) :
          p = q in, Polynomial.coeff p i = Polynomial.coeff q i
          theorem Polynomial.as_sum_support_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) :
          p = Finset.sum (Polynomial.support p) fun (i : ) => Polynomial.C (Polynomial.coeff p i) * Polynomial.X ^ i
          theorem Polynomial.sum_over_range' {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : RS} (h : ∀ (n : ), f n 0 = 0) (n : ) (w : Polynomial.natDegree p < n) :

          We can reexpress a sum over p.support as a sum over range n, for any n satisfying p.natDegree < n.

          theorem Polynomial.sum_over_range {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : RS} (h : ∀ (n : ), f n 0 = 0) :

          We can reexpress a sum over p.support as a sum over range (p.natDegree + 1).

          theorem Polynomial.sum_fin {R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (f : RS) (hf : ∀ (i : ), f i 0 = 0) {n : } {p : Polynomial R} (hn : Polynomial.degree p < n) :
          (Finset.sum Finset.univ fun (i : Fin n) => f (i) (Polynomial.coeff p i)) = Polynomial.sum p f
          theorem Polynomial.as_sum_range_C_mul_X_pow {R : Type u} [Semiring R] (p : Polynomial R) :
          p = Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun (i : ) => Polynomial.C (Polynomial.coeff p i) * Polynomial.X ^ i
          theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.degree p 1) :
          p = Polynomial.C (Polynomial.coeff p 1) * Polynomial.X + Polynomial.C (Polynomial.coeff p 0)
          theorem Polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.degree p = 1) :
          p = Polynomial.C (Polynomial.leadingCoeff p) * Polynomial.X + Polynomial.C (Polynomial.coeff p 0)
          theorem Polynomial.eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.natDegree p 1) :
          p = Polynomial.C (Polynomial.coeff p 1) * Polynomial.X + Polynomial.C (Polynomial.coeff p 0)
          theorem Polynomial.Monic.eq_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hm : Polynomial.Monic p) (hnd : Polynomial.natDegree p = 1) :
          p = Polynomial.X + Polynomial.C (Polynomial.coeff p 0)
          theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.natDegree p 1) :
          ∃ (a : R) (b : R), p = Polynomial.C a * Polynomial.X + Polynomial.C b
          theorem Polynomial.degree_X_pow_le {R : Type u} [Semiring R] (n : ) :
          Polynomial.degree (Polynomial.X ^ n) n
          theorem Polynomial.degree_X_le {R : Type u} [Semiring R] :
          Polynomial.degree Polynomial.X 1
          theorem Polynomial.mem_support_C_mul_X_pow {R : Type u} [Semiring R] {n : } {a : } {c : R} (h : a Polynomial.support (Polynomial.C c * Polynomial.X ^ n)) :
          a = n
          theorem Polynomial.card_support_C_mul_X_pow_le_one {R : Type u} [Semiring R] {c : R} {n : } :
          (Polynomial.support (Polynomial.C c * Polynomial.X ^ n)).card 1
          @[simp]
          theorem Polynomial.degree_X {R : Type u} [Semiring R] [Nontrivial R] :
          Polynomial.degree Polynomial.X = 1
          @[simp]
          theorem Polynomial.natDegree_X {R : Type u} [Semiring R] [Nontrivial R] :
          Polynomial.natDegree Polynomial.X = 1
          theorem Polynomial.coeff_mul_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} {r : R} {a : } :
          Polynomial.coeff (p * (Polynomial.X - Polynomial.C r)) (a + 1) = Polynomial.coeff p a - Polynomial.coeff p (a + 1) * r
          @[simp]
          def Polynomial.nextCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
          R

          The second-highest coefficient, or 0 for constants

          Equations
          Instances For
            @[simp]
            theorem Polynomial.nextCoeff_C_eq_zero {R : Type u} [Semiring R] (c : R) :
            Polynomial.nextCoeff (Polynomial.C c) = 0
            theorem Polynomial.eq_C_of_degree_le_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.degree p 0) :
            p = Polynomial.C (Polynomial.coeff p 0)
            theorem Polynomial.eq_C_of_degree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.degree p = 0) :
            p = Polynomial.C (Polynomial.coeff p 0)
            theorem Polynomial.degree_add_le_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : } (hp : Polynomial.degree p n) (hq : Polynomial.degree q n) :
            theorem Polynomial.natDegree_C_mul_X_pow_le {R : Type u} [Semiring R] (a : R) (n : ) :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ n) n
            theorem Polynomial.degree_add_C {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : 0 < Polynomial.degree p) :
            Polynomial.degree (p + Polynomial.C a) = Polynomial.degree p
            @[simp]
            theorem Polynomial.natDegree_add_C {R : Type u} [Semiring R] {p : Polynomial R} {a : R} :
            @[simp]
            theorem Polynomial.natDegree_C_add {R : Type u} [Semiring R] {p : Polynomial R} {a : R} :
            theorem Polynomial.degree_sum_le {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ιPolynomial R) :
            Polynomial.degree (Finset.sum s fun (i : ι) => f i) Finset.sup s fun (b : ι) => Polynomial.degree (f b)
            theorem Polynomial.degree_pow_le_of_le {R : Type u} [Semiring R] {p : Polynomial R} {a : WithBot } (b : ) (hp : Polynomial.degree p a) :
            Polynomial.degree (p ^ b) b * a
            theorem Polynomial.leadingCoeff_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ) :
            Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X ^ n) = a
            theorem Polynomial.leadingCoeff_C_mul_X {R : Type u} [Semiring R] (a : R) :
            Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X) = a
            @[simp]
            theorem Polynomial.leadingCoeff_C {R : Type u} [Semiring R] (a : R) :
            Polynomial.leadingCoeff (Polynomial.C a) = a
            theorem Polynomial.leadingCoeff_X_pow {R : Type u} [Semiring R] (n : ) :
            Polynomial.leadingCoeff (Polynomial.X ^ n) = 1
            @[simp]
            theorem Polynomial.monic_X_pow {R : Type u} [Semiring R] (n : ) :
            Polynomial.Monic (Polynomial.X ^ n)
            @[simp]
            theorem Polynomial.monic_X {R : Type u} [Semiring R] :
            Polynomial.Monic Polynomial.X
            theorem Polynomial.Monic.ne_zero {R : Type u_2} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : Polynomial.Monic p) :
            p 0
            theorem Polynomial.Monic.ne_zero_of_ne {R : Type u} [Semiring R] (h : 0 1) {p : Polynomial R} (hp : Polynomial.Monic p) :
            p 0
            theorem Polynomial.Monic.ne_zero_of_polynomial_ne {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {r : Polynomial R} (hp : Polynomial.Monic p) (hne : q r) :
            p 0
            theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : (Polynomial.support p).card 1) :
            Polynomial.C (Polynomial.leadingCoeff p) * Polynomial.X ^ Polynomial.natDegree p = p
            theorem Polynomial.degree_le_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : WithBot ) :
            Polynomial.degree f n ∀ (m : ), n < mPolynomial.coeff f m = 0
            theorem Polynomial.degree_lt_iff_coeff_zero {R : Type u} [Semiring R] (f : Polynomial R) (n : ) :
            Polynomial.degree f < n ∀ (m : ), n mPolynomial.coeff f m = 0
            theorem Polynomial.degree_lt_degree_mul_X {R : Type u} [Semiring R] {p : Polynomial R} (hp : p 0) :
            theorem Polynomial.natDegree_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
            Polynomial.natDegree p = 0 ∃ (x : R), Polynomial.C x = p
            theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : } [Semiring R] {p : Polynomial R} (hdeg : n Polynomial.degree p) :
            p 0
            theorem Polynomial.degree_sum_fin_lt {R : Type u} [Semiring R] {n : } (f : Fin nR) :
            Polynomial.degree (Finset.sum Finset.univ fun (i : Fin n) => Polynomial.C (f i) * Polynomial.X ^ i) < n
            theorem Polynomial.degree_linear_le {R : Type u} {a : R} {b : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X + Polynomial.C b) 1
            theorem Polynomial.degree_linear_lt {R : Type u} {a : R} {b : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X + Polynomial.C b) < 2
            theorem Polynomial.degree_C_lt_degree_C_mul_X {R : Type u} {a : R} {b : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C b) < Polynomial.degree (Polynomial.C a * Polynomial.X)
            @[simp]
            theorem Polynomial.degree_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C a * Polynomial.X + Polynomial.C b) = 1
            theorem Polynomial.natDegree_linear_le {R : Type u} {a : R} {b : R} [Semiring R] :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X + Polynomial.C b) 1
            theorem Polynomial.natDegree_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a 0) :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X + Polynomial.C b) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_linear {R : Type u} {a : R} {b : R} [Semiring R] (ha : a 0) :
            Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X + Polynomial.C b) = a
            theorem Polynomial.degree_quadratic_le {R : Type u} {a : R} {b : R} {c : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) 2
            theorem Polynomial.degree_quadratic_lt {R : Type u} {a : R} {b : R} {c : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) < 3
            theorem Polynomial.degree_linear_lt_degree_C_mul_X_sq {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C b * Polynomial.X + Polynomial.C c) < Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2)
            @[simp]
            theorem Polynomial.degree_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) = 2
            theorem Polynomial.natDegree_quadratic_le {R : Type u} {a : R} {b : R} {c : R} [Semiring R] :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) 2
            theorem Polynomial.natDegree_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a 0) :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) = 2
            @[simp]
            theorem Polynomial.leadingCoeff_quadratic {R : Type u} {a : R} {b : R} {c : R} [Semiring R] (ha : a 0) :
            Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) = a
            theorem Polynomial.degree_cubic_le {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) 3
            theorem Polynomial.degree_cubic_lt {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) < 4
            theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) < Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3)
            @[simp]
            theorem Polynomial.degree_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a 0) :
            Polynomial.degree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) = 3
            theorem Polynomial.natDegree_cubic_le {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) 3
            theorem Polynomial.natDegree_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a 0) :
            Polynomial.natDegree (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) = 3
            @[simp]
            theorem Polynomial.leadingCoeff_cubic {R : Type u} {a : R} {b : R} {c : R} {d : R} [Semiring R] (ha : a 0) :
            Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d) = a
            @[simp]
            theorem Polynomial.degree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
            Polynomial.degree (Polynomial.X ^ n) = n
            @[simp]
            theorem Polynomial.natDegree_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ) :
            Polynomial.natDegree (Polynomial.X ^ n) = n
            @[simp]
            theorem Polynomial.natDegree_mul_X {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p 0) :
            @[simp]
            theorem Polynomial.natDegree_X_mul {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (hp : p 0) :
            @[simp]
            theorem Polynomial.natDegree_mul_X_pow {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ) (hp : p 0) :
            @[simp]
            theorem Polynomial.natDegree_X_pow_mul {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ) (hp : p 0) :
            theorem Polynomial.natDegree_X_pow_le {R : Type u_1} [Semiring R] (n : ) :
            Polynomial.natDegree (Polynomial.X ^ n) n
            theorem Polynomial.not_isUnit_X {R : Type u} [Semiring R] [Nontrivial R] :
            ¬IsUnit Polynomial.X
            @[simp]
            theorem Polynomial.degree_mul_X {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} :
            Polynomial.degree (p * Polynomial.X) = Polynomial.degree p + 1
            @[simp]
            theorem Polynomial.degree_mul_X_pow {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ) :
            Polynomial.degree (p * Polynomial.X ^ n) = Polynomial.degree p + n
            theorem Polynomial.degree_sub_C {R : Type u} {a : R} [Ring R] {p : Polynomial R} (hp : 0 < Polynomial.degree p) :
            Polynomial.degree (p - Polynomial.C a) = Polynomial.degree p
            @[simp]
            theorem Polynomial.natDegree_sub_C {R : Type u} [Ring R] {p : Polynomial R} {a : R} :
            theorem Polynomial.degree_X_sub_C_le {R : Type u} [Ring R] (r : R) :
            Polynomial.degree (Polynomial.X - Polynomial.C r) 1
            theorem Polynomial.natDegree_X_sub_C_le {R : Type u} [Ring R] (r : R) :
            Polynomial.natDegree (Polynomial.X - Polynomial.C r) 1
            @[simp]
            theorem Polynomial.degree_X_add_C {R : Type u} [Nontrivial R] [Semiring R] (a : R) :
            Polynomial.degree (Polynomial.X + Polynomial.C a) = 1
            theorem Polynomial.natDegree_X_add_C {R : Type u} [Nontrivial R] [Semiring R] (x : R) :
            Polynomial.natDegree (Polynomial.X + Polynomial.C x) = 1
            @[simp]
            theorem Polynomial.nextCoeff_X_add_C {S : Type v} [Semiring S] (c : S) :
            Polynomial.nextCoeff (Polynomial.X + Polynomial.C c) = c
            theorem Polynomial.degree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : } (hn : 0 < n) (a : R) :
            Polynomial.degree (Polynomial.X ^ n + Polynomial.C a) = n
            theorem Polynomial.X_pow_add_C_ne_zero {R : Type u} [Nontrivial R] [Semiring R] {n : } (hn : 0 < n) (a : R) :
            Polynomial.X ^ n + Polynomial.C a 0
            theorem Polynomial.X_add_C_ne_zero {R : Type u} [Nontrivial R] [Semiring R] (r : R) :
            Polynomial.X + Polynomial.C r 0
            theorem Polynomial.zero_nmem_multiset_map_X_add_C {R : Type u} [Nontrivial R] [Semiring R] {α : Type u_1} (m : Multiset α) (f : αR) :
            0Multiset.map (fun (a : α) => Polynomial.X + Polynomial.C (f a)) m
            theorem Polynomial.natDegree_X_pow_add_C {R : Type u} [Nontrivial R] [Semiring R] {n : } {r : R} :
            Polynomial.natDegree (Polynomial.X ^ n + Polynomial.C r) = n
            theorem Polynomial.X_pow_add_C_ne_one {R : Type u} [Nontrivial R] [Semiring R] {n : } (hn : 0 < n) (a : R) :
            Polynomial.X ^ n + Polynomial.C a 1
            theorem Polynomial.X_add_C_ne_one {R : Type u} [Nontrivial R] [Semiring R] (r : R) :
            Polynomial.X + Polynomial.C r 1
            @[simp]
            theorem Polynomial.leadingCoeff_X_pow_add_C {R : Type u} [Semiring R] {n : } (hn : 0 < n) {r : R} :
            Polynomial.leadingCoeff (Polynomial.X ^ n + Polynomial.C r) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_X_add_C {S : Type v} [Semiring S] (r : S) :
            Polynomial.leadingCoeff (Polynomial.X + Polynomial.C r) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_X_pow_add_one {R : Type u} [Semiring R] {n : } (hn : 0 < n) :
            Polynomial.leadingCoeff (Polynomial.X ^ n + 1) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_pow_X_add_C {R : Type u} [Semiring R] (r : R) (i : ) :
            Polynomial.leadingCoeff ((Polynomial.X + Polynomial.C r) ^ i) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_X_pow_sub_C {R : Type u} [Ring R] {n : } (hn : 0 < n) {r : R} :
            Polynomial.leadingCoeff (Polynomial.X ^ n - Polynomial.C r) = 1
            @[simp]
            theorem Polynomial.leadingCoeff_X_pow_sub_one {R : Type u} [Ring R] {n : } (hn : 0 < n) :
            Polynomial.leadingCoeff (Polynomial.X ^ n - 1) = 1
            @[simp]
            theorem Polynomial.degree_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (a : R) :
            Polynomial.degree (Polynomial.X - Polynomial.C a) = 1
            theorem Polynomial.natDegree_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (x : R) :
            Polynomial.natDegree (Polynomial.X - Polynomial.C x) = 1
            @[simp]
            theorem Polynomial.nextCoeff_X_sub_C {S : Type v} [Ring S] (c : S) :
            Polynomial.nextCoeff (Polynomial.X - Polynomial.C c) = -c
            theorem Polynomial.degree_X_pow_sub_C {R : Type u} [Ring R] [Nontrivial R] {n : } (hn : 0 < n) (a : R) :
            Polynomial.degree (Polynomial.X ^ n - Polynomial.C a) = n
            theorem Polynomial.X_pow_sub_C_ne_zero {R : Type u} [Ring R] [Nontrivial R] {n : } (hn : 0 < n) (a : R) :
            Polynomial.X ^ n - Polynomial.C a 0
            theorem Polynomial.X_sub_C_ne_zero {R : Type u} [Ring R] [Nontrivial R] (r : R) :
            Polynomial.X - Polynomial.C r 0
            theorem Polynomial.zero_nmem_multiset_map_X_sub_C {R : Type u} [Ring R] [Nontrivial R] {α : Type u_1} (m : Multiset α) (f : αR) :
            0Multiset.map (fun (a : α) => Polynomial.X - Polynomial.C (f a)) m
            theorem Polynomial.natDegree_X_pow_sub_C {R : Type u} [Ring R] [Nontrivial R] {n : } {r : R} :
            Polynomial.natDegree (Polynomial.X ^ n - Polynomial.C r) = n
            @[simp]
            theorem Polynomial.leadingCoeff_X_sub_C {S : Type v} [Ring S] (r : S) :
            Polynomial.leadingCoeff (Polynomial.X - Polynomial.C r) = 1

            degree as a monoid homomorphism between R[X] and Multiplicative (WithBot ℕ). This is useful to prove results about multiplication and degree.

            Equations
            • Polynomial.degreeMonoidHom = { toOneHom := { toFun := Polynomial.degree, map_one' := }, map_mul' := }
            Instances For

              Polynomial.leadingCoeff bundled as a MonoidHom when R has NoZeroDivisors, and thus leadingCoeff is multiplicative

              Equations
              • Polynomial.leadingCoeffHom = { toOneHom := { toFun := Polynomial.leadingCoeff, map_one' := }, map_mul' := }
              Instances For
                @[simp]
                theorem Polynomial.leadingCoeffHom_apply {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) :
                Polynomial.leadingCoeffHom p = Polynomial.leadingCoeff p