Mathlib.Algebra.Polynomial.Degree.Units

Polynomial.natDegree_eq_zero_of_isUnit theorem

(h : IsUnit p) : natDegree p = 0

Full source

lemma natDegree_eq_zero_of_isUnit (h : IsUnit p) : natDegree p = 0 := by
  nontriviality R
  obtain ⟨q, hq⟩ := h.exists_right_inv
  have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
  rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
  exact this.1

Units in Polynomial Ring Have Degree Zero

Informal description

For any polynomial $p$ in the polynomial ring $R[X]$ over a semiring $R$, if $p$ is a unit (i.e., invertible), then its natural degree is zero, i.e., $\operatorname{natDegree}(p) = 0$.

Polynomial.degree_eq_zero_of_isUnit theorem

[Nontrivial R] (h : IsUnit p) : degree p = 0

Full source

lemma degree_eq_zero_of_isUnit [Nontrivial R] (h : IsUnit p) : degree p = 0 :=
  (natDegree_eq_zero_iff_degree_le_zero.mp <| natDegree_eq_zero_of_isUnit h).antisymm
    (zero_le_degree_iff.mpr h.ne_zero)

Degree of a Unit Polynomial is Zero in a Nontrivial Semiring

Informal description

Let $R$ be a nontrivial semiring and $p \in R[X]$ be a polynomial. If $p$ is a unit in the polynomial ring $R[X]$, then the degree of $p$ is zero, i.e., $\deg(p) = 0$.

Polynomial.degree_coe_units theorem

[Nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0

Full source

@[simp]
lemma degree_coe_units [Nontrivial R] (u : R[X]R[X]ˣ) : degree (u : R[X]) = 0 :=
  degree_eq_zero_of_isUnit ⟨u, rfl⟩

Degree of Unit Polynomials is Zero

Informal description

Let $R$ be a nontrivial semiring and let $u$ be a unit in the polynomial ring $R[X]$. Then the degree of the polynomial $u$ is zero, i.e., $\deg(u) = 0$.

Polynomial.isUnit_iff theorem

: IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p

Full source

/-- Characterization of a unit of a polynomial ring over an integral domain `R`.
See `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` when `R` is a commutative ring. -/
lemma isUnit_iff : IsUnitIsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
  ⟨fun hp =>
    ⟨p.coeff 0,
      let h := eq_C_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
      ⟨isUnit_C.1 (h ▸ hp), h.symm⟩⟩,
    fun ⟨_, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩

Characterization of Units in Polynomial Ring over Integral Domain: $p$ is a unit iff $p = C(r)$ for some unit $r \in R$

Informal description

A polynomial $p$ in the polynomial ring $R[X]$ over an integral domain $R$ is a unit if and only if there exists a unit $r \in R$ such that $p$ is equal to the constant polynomial $C(r)$.

Polynomial.not_isUnit_of_degree_pos theorem

(p : R[X]) (hpl : 0 < p.degree) : ¬IsUnit p

Full source

lemma not_isUnit_of_degree_pos (p : R[X]) (hpl : 0 < p.degree) : ¬ IsUnit p := by
  cases subsingleton_or_nontrivial R
  · simp [Subsingleton.elim p 0] at hpl
  intro h
  simp [degree_eq_zero_of_isUnit h] at hpl

Polynomials with positive degree are not units

Informal description

Let $R$ be a semiring and let $p \in R[X]$ be a polynomial with positive degree, i.e., $\deg(p) > 0$. Then $p$ is not a unit in the polynomial ring $R[X]$.

Polynomial.not_isUnit_of_natDegree_pos theorem

(p : R[X]) (hpl : 0 < p.natDegree) : ¬IsUnit p

Full source

lemma not_isUnit_of_natDegree_pos (p : R[X]) (hpl : 0 < p.natDegree) : ¬ IsUnit p :=
  not_isUnit_of_degree_pos _ (natDegree_pos_iff_degree_pos.mp hpl)

Non-units among polynomials with positive natural degree

Informal description

Let $R$ be a semiring and let $p \in R[X]$ be a polynomial with positive natural degree, i.e., $\text{natDegree}(p) > 0$. Then $p$ is not a unit in the polynomial ring $R[X]$.

Polynomial.natDegree_coe_units theorem

(u : R[X]ˣ) : natDegree (u : R[X]) = 0

Full source

@[simp] lemma natDegree_coe_units (u : R[X]R[X]ˣ) : natDegree (u : R[X]) = 0 := by
  nontriviality R
  exact natDegree_eq_of_degree_eq_some (degree_coe_units u)

Natural Degree of Unit Polynomials is Zero

Informal description

For any unit $u$ in the polynomial ring $R[X]$ over a semiring $R$, the natural degree of $u$ is zero, i.e., $\mathrm{natDegree}(u) = 0$.

Polynomial.coeff_coe_units_zero_ne_zero theorem

[Nontrivial R] (u : R[X]ˣ) : coeff (u : R[X]) 0 ≠ 0

Full source

theorem coeff_coe_units_zero_ne_zero [Nontrivial R] (u : R[X]R[X]ˣ) : coeffcoeff (u : R[X]) 0 ≠ 0 := by
  conv in 0 => rw [← natDegree_coe_units u]
  rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]
  exact Units.ne_zero _

Nonvanishing of Constant Term for Unit Polynomials in Nontrivial Semirings

Informal description

Let $R$ be a nontrivial semiring and let $u$ be a unit in the polynomial ring $R[X]$. Then the constant term (coefficient of $X^0$) of $u$ is nonzero, i.e., $\text{coeff}(u, 0) \neq 0$.

Polynomial.Monic.C_dvd_iff_isUnit theorem

{a : R} : C a ∣ p ↔ IsUnit a

Full source

lemma Monic.C_dvd_iff_isUnit {a : R} : CC a ∣ pC a ∣ p ↔ IsUnit a where
  mp h := isUnit_iff_dvd_one.mpr <| hp.coeff_natDegree ▸ (C_dvd_iff_dvd_coeff _ _).mp h p.natDegree
  mpr ha := (ha.map C).dvd

Divisibility by Constant Polynomial in Monic Polynomials: $C(a) \mid p \leftrightarrow a$ is a unit

Informal description

For any element $a$ in a commutative semiring $R$ and any monic polynomial $p \in R[X]$, the constant polynomial $C(a)$ divides $p$ if and only if $a$ is a unit in $R$.

Polynomial.Monic.degree_pos_of_not_isUnit theorem

(hu : ¬IsUnit p) : 0 < degree p

Full source

lemma Monic.degree_pos_of_not_isUnit (hu : ¬IsUnit p) : 0 < degree p :=
  hp.degree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one

Degree Positivity for Non-Unit Monic Polynomials: $\neg \text{IsUnit}(p) \to 0 < \deg p$

Informal description

For a monic polynomial $p$ over a semiring $R$, if $p$ is not a unit, then its degree is strictly positive, i.e., $0 < \deg p$.

Polynomial.Monic.natDegree_pos_of_not_isUnit theorem

(hu : ¬IsUnit p) : 0 < natDegree p

Full source

lemma Monic.natDegree_pos_of_not_isUnit (hu : ¬IsUnit p) : 0 < natDegree p :=
  hp.natDegree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one

Positive Degree of Non-Unit Monic Polynomials

Informal description

For a monic polynomial $p$ over a semiring $R$, if $p$ is not a unit (i.e., not invertible), then its natural degree is positive, i.e., $\mathrm{natDegree}(p) > 0$.

Polynomial.degree_pos_of_not_isUnit_of_dvd_monic theorem

(ha : ¬IsUnit a) (hap : a ∣ p) : 0 < degree a

Full source

lemma degree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < degree a := by
  contrapose! ha with h
  rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
  simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

Positive Degree of Non-Unit Divisors of Monic Polynomials

Informal description

Let $R$ be a commutative semiring and let $a, p \in R[X]$ be polynomials such that $p$ is monic. If $a$ is not a unit in $R[X]$ and $a$ divides $p$, then the degree of $a$ is strictly positive, i.e., $0 < \deg(a)$.

Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic theorem

(ha : ¬IsUnit a) (hap : a ∣ p) : 0 < natDegree a

Full source

lemma natDegree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < natDegree a :=
  natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_not_isUnit_of_dvd_monic hp ha hap

Positive Natural Degree of Non-Unit Divisors of Monic Polynomials

Informal description

Let $R$ be a commutative semiring and let $a, p \in R[X]$ be polynomials such that $p$ is monic. If $a$ is not a unit in $R[X]$ and $a$ divides $p$, then the natural degree of $a$ is strictly positive, i.e., $0 < \text{natDegree}(a)$.