natDegree_eq_zero_of_isUnit — Mathlib

English

If p is a unit in the polynomial ring, then natDegree(p) = 0.

Русский

Если p является единицей в кольце многочленов, то natDegree(p) = 0.

LaTeX

$$$ IsUnit(p) \rightarrow natDegree(p) = 0 $$$

Lean4

theorem 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

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