not_isUnit — Mathlib

English

If B is nontrivial, then minpoly_A(x) is not a unit.

Русский

Если B не тривиально, то minpoly_A(x) не является единицей.

LaTeX

$$$\\lnot IsUnit(\\minpoly_A(x)).$$$

Lean4

/-- A minimal polynomial is not a unit. -/
theorem not_isUnit [Nontrivial B] : ¬IsUnit (minpoly A x) :=
  by
  haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
  by_cases hx : IsIntegral A x
  · exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
  · rw [eq_zero hx]
    exact not_isUnit_zero

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