not_isUnit — Mathlib

English

If p is a unit trinomial, then p is not a unit in the polynomial ring; i.e., a unit trinomial cannot itself be a unit.

Русский

Если p является единичным триномиалом, то оно не является единицей в кольце многочленов; единичный триномиал не может быть элементом единицы.

LaTeX

$$$\\neg p.IsUnitTrinomial \\Rightarrow \\text{(not applicable)}$$$

Lean4

theorem not_isUnit (hp : p.IsUnitTrinomial) : ¬IsUnit p :=
  by
  obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
  exact fun h =>
    ne_zero_of_lt hmn
      ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))

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