Theorems · Theorem · group theory

Set.mem_sum_list_ofFn

∀ {α : Type u_1} [inst : AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Set α},
  a ∈ (List.ofFn s).sum ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a

Defined in: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Cited by: 3 results in Mathlib
Foundations: Depth 47 from the axioms · uses propext, Quot.sound
Assumes: AddMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.Elemstatement and proof · cited by 7,166
AddMonoidstatement and proof · cited by 2,864
Set.addstatement · cited by 338
Fin.consproof · cited by 190
Set.zerostatement · cited by 87
Fin.cons_succproof · cited by 54
Fin.cons_zeroproof · cited by 53
Set.mem_addproof · cited by 25
Set.mem_zeroproof · cited by 6
exists_exists_eq_andproof · cited by 5
SetCoe.existsproof · cited by 5

Cited by3

Results whose statement or proof uses this declaration.

Set.mem_nsmulproof · cited by 1
Set.mem_list_sumproof · cited by 0
Finset.mem_sum_list_ofFnproof · cited by 0