eq_zero_iff — Mathlib

English

A multivariate polynomial is zero if and only if all its coefficients are zero.

Русский

Мультипеременный многочлен равен нулю тогда и только тогда, когда все его коэффициенты равны нулю.

LaTeX

$$$p = 0 \\iff \\forall d, \\operatorname{coeff} d\\,p = 0$$$

Lean4

theorem eq_zero_iff {p : MvPolynomial σ R} : p = 0 ↔ ∀ d, coeff d p = 0 :=
  by
  rw [MvPolynomial.ext_iff]
  simp only [coeff_zero]

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