coeff_erase — Mathlib

English

Erasing the nth term of the monomial of degree n with coefficient a yields zero: erase n (monomial n a) = 0.

Русский

Стирание n-ого термена моно-мома степени n с коэффициентом a даёт нуль: erase n (monomial n a) = 0.

LaTeX

$$$\\operatorname{erase}_n(\\operatorname{monomial}_n(a)) = 0$$$

Lean4

theorem coeff_erase (p : R[X]) (n i : ℕ) : (p.erase n).coeff i = if i = n then 0 else p.coeff i :=
  by
  rcases p with ⟨⟩
  simp only [erase_def, coeff]
  exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)

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