leadingCoeff_normalize — Mathlib

English

For any p ∈ R[X], the leading coefficient commutes with normalization: the leading coefficient of normalize p equals normalize of the leading coefficient of p.

Русский

У многочлена p ведущий коэффициент сохраняется при нормализации: leadingCoeff(normalize p) = normalize(leadingCoeff p).

LaTeX

$$$\operatorname{leadingCoeff}(\operatorname{normalize}(p)) = \operatorname{normalize}(\operatorname{leadingCoeff}(p)).$$$

Lean4

@[simp]
theorem leadingCoeff_normalize (p : R[X]) : leadingCoeff (normalize p) = normalize (leadingCoeff p) := by
  simp [normalize_apply]

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