isUnit_iff' — Mathlib

English

For P ∈ R[X], IsUnit P holds if eval_0 P is a unit and P divided by X is nilpotent.

Русский

Для P ∈ R[X], IsUnit P выполняется тогда, когда eval_0 P — единица и P делится на X и результат нильпотентен.

LaTeX

$$$\operatorname{IsUnit}(P) \iff \operatorname{IsUnit}(\operatorname{eval}_0(P)) \land \operatorname{IsNilpotent}(P /_{m} X)$$$

Lean4

theorem isUnit_iff' : IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X) :=
  by
  suffices P = C (eval 0 P) + X * (P /ₘ X) by conv_lhs => rw [this]; simp
  conv_lhs => rw [← modByMonic_add_div P monic_X]
  simp [modByMonic_X]

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