support — Mathlib

English

The support of a FreeAbelianGroup element a is exactly the finite set of generators x ∈ X that appear with nonzero multiplicity in a.

Русский

Поддержка элемента a в FreeAbelianGroup — это конечный набор генераторов x ∈ X, которые встречаются с ненулочной кратностью в a.

LaTeX

$$$\\operatorname{support}(a) = \\{ x \\in X \\mid \\text{coeff}(x,a) \\neq 0\\}$$$

Lean4

/-- `support a` for `a : FreeAbelianGroup X` is the finite set of `x : X`
that occur in the formal sum `a`. -/
def support (a : FreeAbelianGroup X) : Finset X :=
  a.toFinsupp.support

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