Theorems · Theorem · number theory

Finset.mem_addSpan

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {a : α},
  a ∈ s.addSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∑ a ∈ s, ε a • a = a

Defined in

Mathlib.Combinatorics.Additive.Dissociation

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupDecidableEqFintype