eraseLead_monomial — Mathlib

English

For any i ∈ ℕ and r ∈ R, eraseLead of the monomial i with coefficient r is zero.

Русский

Для любых i ∈ ℕ и r ∈ R удаление ведущего монома i с коэффициентом r даёт 0.

LaTeX

$$$\operatorname{eraseLead}(\operatorname{monomial}(i, r)) = 0$$$

Lean4

@[simp]
theorem eraseLead_monomial (i : ℕ) (r : R) : eraseLead (monomial i r) = 0 := by
  classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

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