isUnit_iff_degree_eq_zero — Mathlib

English

Over a field R, a polynomial p is a unit in R[X] if and only if deg(p) = 0.

Русский

Над полем R многочлен p является единицей в R[X] тогда и только тогда, когда deg(p) = 0.

LaTeX

$$$\text{IsUnit}(p) \iff \deg(p) = 0$.$$

Lean4

theorem isUnit_iff_degree_eq_zero : IsUnit p ↔ degree p = 0 :=
  ⟨degree_eq_zero_of_isUnit, fun h =>
    have : degree p ≤ 0 := by simp [*, le_refl]
    have hc : coeff p 0 ≠ 0 := fun hc => by rw [eq_C_of_degree_le_zero this, hc] at h; simp only [map_zero] at h;
      contradiction
    isUnit_iff_dvd_one.2
      ⟨C (coeff p 0)⁻¹, by
        conv in p => rw [eq_C_of_degree_le_zero this]
        rw [← C_mul, mul_inv_cancel₀ hc, C_1]⟩⟩

Похожие утверждения