natDegree_map_eq_of_injective — Mathlib

English

Let f be an injective ring hom. Then for any p ∈ R[X], natDegree(p.map f) = natDegree(p).

Русский

Пусть f — инъективный кольцевой гомоморф. Тогда для любого p ∈ R[X] natDegree(p.map f) = natDegree(p).

LaTeX

$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] {f : R \rightarrow+* S} (hf : Injective f) {p : R[X]}, natDegree (p.map f) = natDegree p$$$

Lean4

theorem natDegree_map_eq_of_injective (hf : Injective f) (p : R[X]) : natDegree (p.map f) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_map_eq_of_injective hf p)

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