degree_map — Mathlib

English

Let P be a monic polynomial in R[X]. For any ring hom f: R →+* S, the degree of P.map f equals the degree of P.

Русский

Пусть P — мононичный полином над R[X]. Для любого кольцевого гомоморфа f: R →+* S степень( P.map f ) равна степени(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).degree = P.degree$$$

Lean4

@[simp]
theorem degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) : (P.map f).degree = P.degree :=
  by simp_all

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