map_natDegree_eq_natDegree — Mathlib

English

If φ is as above and φ maps each monomial monomial n to degree fu(n) with fu(n) = n, then φ preserves natDegree: (φ p).natDegree = p.natDegree for all p.

Русский

Если fu(n) = n и φ(mononial n) имеет natDegree = n, то (φ p).natDegree = p.natDegree для всех p.

LaTeX

$$$\\forall p:\\, R[X],\\ (φ p).natDegree = p.natDegree$$$

Lean4

theorem map_natDegree_eq_natDegree {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]]
    {φ : F} (p) (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n) : (φ p).natDegree = p.natDegree :=
  (map_natDegree_eq_sub (fun _ h => (Nat.not_lt_zero _ h).elim) (by simpa)).trans p.natDegree.sub_zero

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