Mathlib.Algebra.Polynomial.Degree.SmallDegree

Polynomial.exists_eq_X_add_C_of_natDegree_le_one theorem

(h : natDegree p ≤ 1) : ∃ a b, p = C a * X + C b

Full source

theorem exists_eq_X_add_C_of_natDegree_le_one (h : natDegree p ≤ 1) : ∃ a b, p = C a * X + C b :=
  ⟨p.coeff 1, p.coeff 0, eq_X_add_C_of_natDegree_le_one h⟩

Representation of Degree-1 Polynomials as Linear Forms

Informal description

For any polynomial $p \in R[X]$ with natural degree at most 1 (i.e., $\text{natDegree}(p) \leq 1$), there exist elements $a, b \in R$ such that $p = aX + b$, where $aX + b$ is expressed as $C(a) \cdot X + C(b)$ in the polynomial ring $R[X]$.

Polynomial.zero_le_degree_iff theorem

: 0 ≤ degree p ↔ p ≠ 0

Full source

theorem zero_le_degree_iff : 0 ≤ degree p ↔ p ≠ 0 := by
  rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]

Non-negativity of Polynomial Degree if and only if Non-zero Polynomial

Informal description

For any polynomial $p \in R[X]$, the degree of $p$ is non-negative (i.e., $0 \leq \deg(p)$) if and only if $p$ is not the zero polynomial.

Polynomial.ne_zero_of_coe_le_degree theorem

(hdeg : ↑n ≤ p.degree) : p ≠ 0

Full source

theorem ne_zero_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : p ≠ 0 :=
  zero_le_degree_iff.mp <| (WithBot.coe_le_coe.mpr n.zero_le).trans hdeg

Non-zero Polynomial from Lower Bound on Degree

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, if the degree of $p$ is at least $n$ (when viewed in `WithBot ℕ`), then $p$ is not the zero polynomial.

Polynomial.le_natDegree_of_coe_le_degree theorem

(hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree

Full source

theorem le_natDegree_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree :=
  WithBot.coe_le_coe.mp <| by
    rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg

Lower Bound on Natural Degree from Degree Inequality

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, if the degree of $p$ (viewed in $\mathbb{N} \cup \{\bot\}$) is at least $n$, then $n$ is less than or equal to the natural degree of $p$.

Polynomial.degree_linear_le theorem

: degree (C a * X + C b) ≤ 1

Full source

theorem degree_linear_le : degree (C a * X + C b) ≤ 1 :=
  degree_add_le_of_degree_le (degree_C_mul_X_le _) <| le_trans degree_C_le Nat.WithBot.coe_nonneg

Degree Bound for Linear Polynomials: $\deg(aX + b) \leq 1$

Informal description

For any elements $a, b$ in a semiring $R$, the degree of the linear polynomial $aX + b$ is less than or equal to 1, i.e., $\deg(aX + b) \leq 1$.

Polynomial.degree_linear_lt theorem

: degree (C a * X + C b) < 2

Full source

theorem degree_linear_lt : degree (C a * X + C b) < 2 :=
  degree_linear_le.trans_lt <| WithBot.coe_lt_coe.mpr one_lt_two

Degree Bound for Linear Polynomials: $\deg(aX + b) < 2$

Informal description

For any elements $a, b$ in a semiring $R$, the degree of the linear polynomial $aX + b$ is strictly less than 2, i.e., $\deg(aX + b) < 2$.

Polynomial.degree_linear theorem

(ha : a ≠ 0) : degree (C a * X + C b) = 1

Full source

@[simp]
theorem degree_linear (ha : a ≠ 0) : degree (C a * X + C b) = 1 := by
  rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]

Degree of Linear Polynomial: $\deg(aX + b) = 1$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the degree of the linear polynomial $aX + b$ is equal to $1$, i.e., $\deg(aX + b) = 1$.

Polynomial.natDegree_linear_le theorem

: natDegree (C a * X + C b) ≤ 1

Full source

theorem natDegree_linear_le : natDegree (C a * X + C b) ≤ 1 :=
  natDegree_le_of_degree_le degree_linear_le

Natural Degree Bound for Linear Polynomials: $\text{natDegree}(aX + b) \leq 1$

Informal description

For any elements $a, b$ in a semiring $R$, the natural degree of the linear polynomial $aX + b$ is less than or equal to 1, i.e., $\text{natDegree}(aX + b) \leq 1$.

Polynomial.natDegree_linear theorem

(ha : a ≠ 0) : natDegree (C a * X + C b) = 1

Full source

theorem natDegree_linear (ha : a ≠ 0) : natDegree (C a * X + C b) = 1 := by
  rw [natDegree_add_C, natDegree_C_mul_X a ha]

Natural Degree of Linear Polynomial: $\text{natDegree}(aX + b) = 1$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the natural degree of the linear polynomial $aX + b$ is equal to $1$, i.e., $$\text{natDegree}(aX + b) = 1.$$

Polynomial.leadingCoeff_linear theorem

(ha : a ≠ 0) : leadingCoeff (C a * X + C b) = a

Full source

@[simp]
theorem leadingCoeff_linear (ha : a ≠ 0) : leadingCoeff (C a * X + C b) = a := by
  rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
    leadingCoeff_C_mul_X]

Leading coefficient of linear polynomial: $\text{lc}(aX + b) = a$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the leading coefficient of the linear polynomial $aX + b$ is equal to $a$, i.e., \[ \text{lc}(aX + b) = a. \]

Polynomial.degree_quadratic_le theorem

: degree (C a * X ^ 2 + C b * X + C c) ≤ 2

Full source

theorem degree_quadratic_le : degree (C a * X ^ 2 + C b * X + C c) ≤ 2 := by
  simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
      (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

Degree Bound for Quadratic Polynomials: $\deg(aX^2 + bX + c) \leq 2$

Informal description

For any elements $a, b, c$ in a semiring $R$, the degree of the quadratic polynomial $aX^2 + bX + c$ is less than or equal to 2, i.e., $$\deg(aX^2 + bX + c) \leq 2.$$

Polynomial.degree_quadratic_lt theorem

: degree (C a * X ^ 2 + C b * X + C c) < 3

Full source

theorem degree_quadratic_lt : degree (C a * X ^ 2 + C b * X + C c) < 3 :=
  degree_quadratic_le.trans_lt <| WithBot.coe_lt_coe.mpr <| lt_add_one 2

Strict Degree Bound for Quadratic Polynomials: $\deg(aX^2 + bX + c) < 3$

Informal description

For any elements $a, b, c$ in a semiring $R$, the degree of the quadratic polynomial $aX^2 + bX + c$ is strictly less than 3, i.e., $$\deg(aX^2 + bX + c) < 3.$$

Polynomial.degree_linear_lt_degree_C_mul_X_sq theorem

(ha : a ≠ 0) : degree (C b * X + C c) < degree (C a * X ^ 2)

Full source

theorem degree_linear_lt_degree_C_mul_X_sq (ha : a ≠ 0) :
    degree (C b * X + C c) < degree (C a * X ^ 2) := by
  simpa only [degree_C_mul_X_pow 2 ha] using degree_linear_lt

Degree Comparison: $\deg(bX + c) < \deg(aX^2)$ for $a \neq 0$

Informal description

For any elements $a, b, c$ in a semiring $R$ with $a \neq 0$, the degree of the linear polynomial $bX + c$ is strictly less than the degree of the quadratic monomial $aX^2$, i.e., $$\deg(bX + c) < \deg(aX^2).$$

Polynomial.degree_quadratic theorem

(ha : a ≠ 0) : degree (C a * X ^ 2 + C b * X + C c) = 2

Full source

@[simp]
theorem degree_quadratic (ha : a ≠ 0) : degree (C a * X ^ 2 + C b * X + C c) = 2 := by
  rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    degree_C_mul_X_pow 2 ha]
  rfl

Degree of Quadratic Polynomial: $\deg(aX^2 + bX + c) = 2$ for $a \neq 0$

Informal description

For any elements $a, b, c$ in a semiring $R$ with $a \neq 0$, the degree of the quadratic polynomial $aX^2 + bX + c$ is equal to 2, i.e., $$\deg(aX^2 + bX + c) = 2.$$

Polynomial.natDegree_quadratic_le theorem

: natDegree (C a * X ^ 2 + C b * X + C c) ≤ 2

Full source

theorem natDegree_quadratic_le : natDegree (C a * X ^ 2 + C b * X + C c) ≤ 2 :=
  natDegree_le_of_degree_le degree_quadratic_le

Natural Degree Bound for Quadratic Polynomials: $\text{natDegree}(aX^2 + bX + c) \leq 2$

Informal description

For any elements $a, b, c$ in a semiring $R$, the natural degree of the quadratic polynomial $aX^2 + bX + c$ is at most 2, i.e., $$\text{natDegree}(aX^2 + bX + c) \leq 2.$$

Polynomial.natDegree_quadratic theorem

(ha : a ≠ 0) : natDegree (C a * X ^ 2 + C b * X + C c) = 2

Full source

theorem natDegree_quadratic (ha : a ≠ 0) : natDegree (C a * X ^ 2 + C b * X + C c) = 2 :=
  natDegree_eq_of_degree_eq_some <| degree_quadratic ha

Natural Degree of Quadratic Polynomial: $\text{natDegree}(aX^2 + bX + c) = 2$ for $a \neq 0$

Informal description

For any elements $a, b, c$ in a semiring $R$ with $a \neq 0$, the natural degree of the quadratic polynomial $aX^2 + bX + c$ is equal to 2, i.e., $$\text{natDegree}(aX^2 + bX + c) = 2.$$

Polynomial.leadingCoeff_quadratic theorem

(ha : a ≠ 0) : leadingCoeff (C a * X ^ 2 + C b * X + C c) = a

Full source

@[simp]
theorem leadingCoeff_quadratic (ha : a ≠ 0) : leadingCoeff (C a * X ^ 2 + C b * X + C c) = a := by
  rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]

Leading coefficient of quadratic polynomial: $\text{lc}(aX^2 + bX + c) = a$ for $a \neq 0$

Informal description

For any elements $a, b, c$ in a semiring $R$ with $a \neq 0$, the leading coefficient of the quadratic polynomial $aX^2 + bX + c$ is equal to $a$.

Polynomial.degree_cubic_le theorem

: degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3

Full source

theorem degree_cubic_le : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3 := by
  simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
      (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)

Degree Bound for Cubic Polynomials: $\deg(aX^3 + bX^2 + cX + d) \leq 3$

Informal description

For any elements $a, b, c, d$ in a semiring $R$, the degree of the cubic polynomial $aX^3 + bX^2 + cX + d$ is less than or equal to 3, i.e., $$\deg(aX^3 + bX^2 + cX + d) \leq 3.$$

Polynomial.degree_cubic_lt theorem

: degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) < 4

Full source

theorem degree_cubic_lt : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) < 4 :=
  degree_cubic_le.trans_lt <| WithBot.coe_lt_coe.mpr <| lt_add_one 3

Strict Degree Bound for Cubic Polynomials: $\deg(aX^3 + bX^2 + cX + d) < 4$

Informal description

For any elements $a, b, c, d$ in a semiring $R$, the degree of the cubic polynomial $aX^3 + bX^2 + cX + d$ is strictly less than 4, i.e., $$\deg(aX^3 + bX^2 + cX + d) < 4.$$

Polynomial.degree_quadratic_lt_degree_C_mul_X_cb theorem

(ha : a ≠ 0) : degree (C b * X ^ 2 + C c * X + C d) < degree (C a * X ^ 3)

Full source

theorem degree_quadratic_lt_degree_C_mul_X_cb (ha : a ≠ 0) :
    degree (C b * X ^ 2 + C c * X + C d) < degree (C a * X ^ 3) := by
  simpa only [degree_C_mul_X_pow 3 ha] using degree_quadratic_lt

Degree comparison: $\deg(bX^2 + cX + d) < \deg(aX^3)$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the degree of the quadratic polynomial $bX^2 + cX + d$ is strictly less than the degree of the cubic monomial $aX^3$. In mathematical notation: $$\deg(bX^2 + cX + d) < \deg(aX^3) \quad \text{for } a \neq 0.$$

Polynomial.degree_cubic theorem

(ha : a ≠ 0) : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3

Full source

@[simp]
theorem degree_cubic (ha : a ≠ 0) : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3 := by
  rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
    degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    degree_C_mul_X_pow 3 ha]
  rfl

Degree of a Cubic Polynomial: $\deg(aX^3 + bX^2 + cX + d) = 3$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the degree of the cubic polynomial $aX^3 + bX^2 + cX + d$ is equal to 3, i.e., $$\deg(aX^3 + bX^2 + cX + d) = 3.$$

Polynomial.natDegree_cubic_le theorem

: natDegree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3

Full source

theorem natDegree_cubic_le : natDegree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3 :=
  natDegree_le_of_degree_le degree_cubic_le

Natural Degree Bound for Cubic Polynomials: $\operatorname{natDegree}(aX^3 + bX^2 + cX + d) \leq 3$

Informal description

For any elements $a, b, c, d$ in a semiring $R$, the natural degree of the cubic polynomial $aX^3 + bX^2 + cX + d$ is less than or equal to 3, i.e., $$\operatorname{natDegree}(aX^3 + bX^2 + cX + d) \leq 3.$$

Polynomial.natDegree_cubic theorem

(ha : a ≠ 0) : natDegree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3

Full source

theorem natDegree_cubic (ha : a ≠ 0) : natDegree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3 :=
  natDegree_eq_of_degree_eq_some <| degree_cubic ha

Natural Degree of a Cubic Polynomial: $\operatorname{natDegree}(aX^3 + bX^2 + cX + d) = 3$ for $a \neq 0$

Informal description

For any elements $a, b, c, d$ in a semiring $R$ with $a \neq 0$, the natural degree of the cubic polynomial $aX^3 + bX^2 + cX + d$ is equal to 3, i.e., \[ \operatorname{natDegree}(aX^3 + bX^2 + cX + d) = 3. \]

Polynomial.leadingCoeff_cubic theorem

(ha : a ≠ 0) : leadingCoeff (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = a

Full source

@[simp]
theorem leadingCoeff_cubic (ha : a ≠ 0) :
    leadingCoeff (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = a := by
  rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]

Leading Coefficient of Cubic Polynomial: $\text{lc}(aX^3 + bX^2 + cX + d) = a$ for $a \neq 0$

Informal description

For any elements $a, b, c, d$ in a semiring $R$ with $a \neq 0$, the leading coefficient of the cubic polynomial $aX^3 + bX^2 + cX + d$ is equal to $a$, i.e., \[ \text{lc}(aX^3 + bX^2 + cX + d) = a. \]