normalize_eq_self — Mathlib

English

If p is monic, then normalization leaves p unchanged: normalize p = p.

Русский

Если p монична, то нормализация не изменяет p: normalize p = p.

LaTeX

$$$\text{If } p \text{ is monic, then } \operatorname{normalize}(p) = p.$$$

Lean4

theorem normalize_eq_self {p : R[X]} (hp : p.Monic) : normalize p = p := by
  simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one, Units.val_one,
    Polynomial.C.map_one, mul_one]

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