English
If k acts regularly on R, then natDegree(k • p) = natDegree(p) for any p ∈ R[X].
Русский
Если k действует регулярно на R, тогда natDegree(k • p) = natDegree(p) для любого p ∈ R[X].
LaTeX
$$$\forall {R} [\text{Semiring } R] {S} [\text{SMulZeroClass } S R] {k : S} (p : R[X]), IsSMulRegular R k \rightarrow natDegree (k • p) = natDegree p$$$
Lean4
theorem degree_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) :
(k • p).degree = p.degree := by
refine le_antisymm ?_ ?_
· rw [degree_le_iff_coeff_zero]
intro m hm
rw [degree_lt_iff_coeff_zero] at hm
simp [hm m le_rfl]
· rw [degree_le_iff_coeff_zero]
intro m hm
rw [degree_lt_iff_coeff_zero] at hm
refine h ?_
simpa using hm m le_rfl