monic_normalize — Mathlib

English

For a nonzero polynomial p over a field R, the normalization normalize p is monic.

Русский

Для ненулевого полинома p над полем R нормализация normalize p является моническим полиномом.

LaTeX

$$[Field R] [DecidableEq R] → p ≠ 0 → Monic (normalize p)$$

Lean4

theorem monic_normalize [DecidableEq R] (hp0 : p ≠ 0) : Monic (normalize p) :=
  by
  rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0
  rw [Monic, leadingCoeff_normalize, normalize_eq_one]
  apply hp0

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