degree_smul — Mathlib

English

If r is regular, then deg_m(r · f) = deg_m(f).

Русский

Если r регулярен, то deg_m(r · f) = deg_m(f).

LaTeX

$$$$ \deg_m(r \cdot f) = \deg_m(f), \quad \text{provided } r \text{ is regular}. $$$$

Lean4

theorem degree_smul {r : R} (hr : IsRegular r) {f : MvPolynomial σ R} : m.degree (r • f) = m.degree f :=
  by
  by_cases hf : f = 0
  · simp [hf]
  apply m.toSyn.injective
  apply le_antisymm degree_smul_le
  apply le_degree
  simp only [mem_support_iff, smul_eq_C_mul]
  rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_add]
  simp [leadingCoeff, hr.left.mul_left_eq_zero_iff, hf]

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