map_normalize — Mathlib

English

Let f be a ring homomorphism; mapping after normalization commutes with normalization after mapping: map f (normalize p) = normalize (map f p).

Русский

Пусть f — гомоморфизм колец; отображение после нормализации коммутирует с нормализацией после отображения: map f (normalize p) = normalize (map f p).

LaTeX

$$$\operatorname{map} f (\operatorname{normalize} p) = \operatorname{normalize} (\operatorname{map} f p).$$$

Lean4

@[simp]
theorem map_normalize [DecidableEq R] [Field S] [DecidableEq S] (f : R →+* S) :
    map f (normalize p) = normalize (map f p) := by
  by_cases hp : p = 0
  · simp [hp]
  · simp [normalize_apply, Polynomial.map_mul, normUnit, hp]

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