degrees_map_le — Mathlib

English

For any ring homomorphism f, the degrees of the image map f p do not exceed the degrees of p.

Русский

Для любого гомоморфизма колец степени образа через f не превосходят степеней p.

LaTeX

$$$[\text{CommSemiring } S] \; {f : R \to^+_* S} \; (\operatorname{map} f \; p).degrees \le p.degrees$$$

Lean4

theorem degrees_map_le [CommSemiring S] {f : R →+* S} : (map f p).degrees ≤ p.degrees := by
  classical exact Finset.sup_mono <| support_map_subset ..

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