normalize_eq_self_iff_monic — Mathlib

English

For a polynomial p with coefficients in a field, if p ≠ 0 then normalize p = p iff p is Monic.

Русский

Для полинома p над полем, если p ≠ 0, то normalize p = p эквивалентно тому, что p монический.

LaTeX

$$p ≠ 0 → (normalize p = p) ⇔ p.Monic$$

Lean4

theorem normalize_eq_self_iff_monic [DecidableEq R] {p : Polynomial R} (hp : p ≠ 0) : normalize p = p ↔ p.Monic :=
  ⟨fun h ↦ h ▸ monic_normalize hp, fun h ↦ Monic.normalize_eq_self h⟩

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