coeff_natTrailingDegree_eq_zero — Mathlib

English

coeff p (natTrailingDegree p) = 0 if and only if p = 0.

Русский

coeff(p, natTrailingDegree(p)) = 0 тогда же, что и p = 0.

LaTeX

$$$\operatorname{coeff}(p, \operatorname{natTrailingDegree}(p)) = 0 \iff p = 0$$$

Lean4

@[simp]
theorem coeff_natTrailingDegree_eq_zero : coeff p p.natTrailingDegree = 0 ↔ p = 0 :=
  by
  constructor
  · rintro h
    by_contra hp
    obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp
    obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm
    exact hpn h
  · rintro rfl
    simp

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