natDegree_smul_of_smul_regular — Mathlib

English

If k acts regularly on R, then degree(k • p) = degree(p) for any p ∈ R[X].

Русский

Если k действует регулярно на R, тогда degree(k • p) = degree(p) для любого p ∈ R[X].

LaTeX

$$$\forall {R} [\text{Semiring } R] {S} [\text{SMulZeroClass } S R] {k : S} (p : R[X]), IsSMulRegular R k \rightarrow degree (k • p) = degree p$$$

Lean4

theorem natDegree_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) :
    (k • p).natDegree = p.natDegree := by
  by_cases hp : p = 0
  · simp [hp]
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree, degree_smul_of_smul_regular p h]
  contrapose! hp
  rw [← smul_zero k] at hp
  exact h.polynomial hp

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