degree_map_eq_of_injective — Mathlib

English

Let f be an injective ring hom. Then for any polynomial p ∈ R[X], the degree is preserved under map: degree(p.map f) = degree(p).

Русский

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

LaTeX

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

Lean4

theorem degree_map_eq_of_injective (hf : Injective f) (p : R[X]) : degree (p.map f) = degree p :=
  letI := Classical.decEq R
  if h : p = 0 then by simp [h]
  else
    degree_map_eq_of_leadingCoeff_ne_zero _ (by rw [← f.map_zero]; exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h))

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