degree_smul_of_smul_regular — Mathlib

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

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