English
Let φ be an additive map as above and suppose φ kills all monomials of degree < k and deg φ(monomial n) = fu(n) with fu shifted by k. Then (φ p).natDegree = p.natDegree − k for all p.
Русский
Пусть φ — аддитивное отображение, обнуляющее мономы степени < k, и deg φ(monomial n) = fu(n) после сдвига на k. Тогда (φ p).natDegree = p.natDegree − k для всех p.
LaTeX
$$$\\forall p:\\, R[X],\\ (φ p).natDegree = p.natDegree - k$$$
Lean4
theorem map_natDegree_eq_sub {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F}
{p : R[X]} {k : ℕ} (φ_k : ∀ f : R[X], f.natDegree < k → φ f = 0)
(φ_mon : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n - k) : (φ p).natDegree = p.natDegree - k :=
mono_map_natDegree_eq k (fun j => j - k) (by simp_all) (@fun _ _ h => (tsub_lt_tsub_iff_right h).mpr) (φ_k _) φ_mon
