leadingCoeff_ne_zero_iff — Mathlib

English

The leading coefficient of f with respect to m is nonzero if and only if f is nonzero.

Русский

Ведущий коэффициент f относительно m не равен нулю тогда и только тогда, когда f не равен нулю.

LaTeX

$$$m.leadingCoeff f \neq 0 \iff f \neq 0$$$

Lean4

theorem leadingCoeff_ne_zero_iff {f : MvPolynomial σ R} : m.leadingCoeff f ≠ 0 ↔ f ≠ 0 :=
  by
  constructor
  · rw [not_imp_not]
    intro hf
    rw [hf, leadingCoeff_zero]
  · intro hf
    rw [← support_nonempty] at hf
    rw [leadingCoeff, ← mem_support_iff, degree]
    suffices f.support.sup m.toSyn ∈ m.toSyn '' f.support
      by
      obtain ⟨d, hd, hd'⟩ := this
      rw [← hd', AddEquiv.symm_apply_apply]
      exact hd
    exact Finset.sup_mem_of_nonempty hf

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