ne_zero_iff

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.ne_zero_iff

English

A polynomial is nonzero if and only if there exists a coefficient that is nonzero.

Русский

Полином не нулевой тогда, когда существует коэффициент, не равный нулю.

LaTeX

$$$p \\neq 0 \\iff \\exists d, \\operatorname{coeff} d\\,p \\neq 0$$$

Lean4

theorem ne_zero_iff {p : MvPolynomial σ R} : p ≠ 0 ↔ ∃ d, coeff d p ≠ 0 :=
  by
  rw [Ne, eq_zero_iff]
  push_neg
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru