English
Let P be a monic polynomial in R[X]. For any ring homomorphism f: R →+* S, the natural degree of P mapped by f equals the natural degree of P; i.e. natDegree(P.map f) = natDegree(P).
Русский
Пусть P — мононичный полином над R[X]. Для любого кольцевого однозначного отображения f: R →+* S верно, что natDegree(P.map f) = natDegree(P).
LaTeX
$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] [\text{Nontrivial } S] \{P : R[X]\} (hmo : P.Monic) (f : R \rightarrow+* S), (P.map f).natDegree = P.natDegree$$$
Lean4
@[simp]
theorem natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
(P.map f).natDegree = P.natDegree :=
by
refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
exact one_ne_zero
