leadingCoeff_eq_zero — Mathlib

English

For injective D, the leading coefficient of p with respect to D is zero iff p = 0.

Русский

Пусть D инъективна; ведущий коэффициент p равен нулю тогда и только тогда, когда p = 0.

LaTeX

$$p.leadingCoeff D = 0 \iff p = 0$$

Lean4

@[simp]
theorem leadingCoeff_eq_zero (hD : D.Injective) : p.leadingCoeff D = 0 ↔ p = 0 :=
  by
  refine ⟨(fun h => ?_).mtr, fun h => h ▸ leadingCoeff_zero⟩
  rw [leadingCoeff, ← Ne, ← Finsupp.mem_support_iff]
  exact supDegree_mem_support hD h

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