map — Mathlib

English

For any ring hom f : R → S and any monic p ∈ R[X], the image p.map f ∈ S[X] is monic.

Русский

Для любого кольцо-гомоморфизма f: R → S и моничного p ∈ R[X], образ p.map f ∈ S[X] моничен.

LaTeX

$$$\text{Map}(f,\,p)\text{ Monic} \Rightarrow p.map f\text{ Monic}.$$$

Lean4

theorem map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f) :=
  by
  unfold Monic
  nontriviality
  have : f p.leadingCoeff ≠ 0 := by
    rw [show _ = _ from hp, f.map_one]
    exact one_ne_zero
  rw [Polynomial.leadingCoeff, coeff_map]
  suffices p.coeff (p.map f).natDegree = 1 by simp [this]
  rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]

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