natDegree_smul — Mathlib

English

If a ≠ 0, then natDegree(a • p) = p.natDegree.

Русский

Если a ≠ 0, то natDegree(a • p) = p.natDegree.

LaTeX

$$a ≠ 0 → (a • p).natDegree = p.natDegree$$

Lean4

theorem natDegree_smul {S : Type*} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] {a : S} (ha : a ≠ 0) :
    (a • p).natDegree = p.natDegree := by
  by_cases hp : p = 0
  · simp only [hp, smul_zero]
  · apply natDegree_eq_of_le_of_coeff_ne_zero
    · exact (natDegree_smul_le _ _).trans (le_refl _)
    · simp only [coeff_smul]
      apply smul_ne_zero ha
      simp [hp]

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