mem_degrees — Mathlib

English

For p ∈ MvPolynomial, i ∈ p.degrees iff there exists d with p.coeff d ≠ 0 and i ∈ d.support.

Русский

Для p ∈ MvPolynomial и i ∈ p.degrees выполняется эквивалентность: i принадлежит deg(p) тогда и только тогда, существует d, такое что p.coeff d ≠ 0 и i ∈ поддержка d.

LaTeX

$$$\, i \in p.degrees \ \Longleftrightarrow \ \exists d,\ p.coeff(d) \neq 0 \land i \in d.supp$$$

Lean4

theorem mem_degrees {p : MvPolynomial σ R} {i : σ} : i ∈ p.degrees ↔ ∃ d, p.coeff d ≠ 0 ∧ i ∈ d.support := by
  classical simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset]

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