natDegree_map_le — Mathlib

English

Let f be a ring homomorphism R →+* S. For any polynomial p ∈ R[X], the degree of its image under map f does not exceed the degree of p, i.e. natDegree(p.map f) ≤ natDegree p.

Русский

Пусть f: R →+* S — кольцо-гомоморфизм. Для любого полинома p ∈ R[X] степень образа p(х) при отображении f не превышает степень p: natDegree(p.map f) ≤ natDegree p.

LaTeX

$$$\\operatorname{natDegree}(p.map\\ f) \\le \\operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_map_le : natDegree (p.map f) ≤ natDegree p :=
  natDegree_le_natDegree degree_map_le

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