Theorems · Theorem · number theory

Finset.exists_subset_mulSpan_card_le_of_forall_mulDissociated

∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {d : ℕ},
  (∀ s' ⊆ s, MulDissociated ↑s' → s'.card ≤ d) → ∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.mulSpan

If every dissociated subset of s has size at most d, then s is actually generated by a subset of size at most d. This is a dissociation analog of the fact that a set whose linearly independent subsets all have size at most d is of dimension at most d itself.

Defined in

Mathlib.Combinatorics.Additive.Dissociation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupDecidableEqFintype