notMem_support_iff — Mathlib

English

An x is not in the support of a if and only if the coefficient of x in a is zero.

Русский

Элемент x не принадлежит поддержке a тогда и только тогда, когда коэффициент x в a равен нулю.

LaTeX

$$$x \\notin \\operatorname{support}(a) \\iff coeff(x,a) = 0$$$

Lean4

theorem notMem_support_iff (x : X) (a : FreeAbelianGroup X) : x ∉ a.support ↔ coeff x a = 0 :=
  by
  rw [support, Finsupp.notMem_support_iff]
  exact Iff.rfl

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