Theorems · Definition · number theory

Finset.addSpan

{α : Type u_1} → [AddCommGroup α] → [DecidableEq α] → [Fintype α] → Finset α → Finset α

The span of a finset s is the finset of elements of the form ∑ a ∈ s, ε a • a where ε ∈ {-1, 0, 1} ^ s. This is an analog of the linear span in a vector space, but with the "scalars" restricted to 0 and ±1.

Defined in

Mathlib.Combinatorics.Additive.Dissociation

Cited by

4 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupDecidableEqFintype