mem_support_iff — Mathlib

English

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

Русский

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

LaTeX

$$$x \\in \\operatorname{support}(a) \\iff coeff(x,a) \\neq 0$$$

Lean4

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

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