Theorems · Theorem · general algebraic systems
DFinsupp.add_closure_iUnion_range_single
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)],
AddSubmonoid.closure (⋃ i, Set.range (DFinsupp.single i)) = ⊤- Defined in
- Mathlib.Data.DFinsupp.Ext
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqAddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Top.topstatement and proof · cited by 9,680
- Set.rangestatement and proof · cited by 4,705
- Set.iUnionstatement and proof · cited by 2,483
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement · cited by 1,178
- DFinsuppstatement and proof · cited by 694
- Set.mem_range_selfproof · cited by 328
- AddSubmonoid.closurestatement and proof · cited by 224
- Set.mem_iUnionproof · cited by 212
- DFinsupp.singlestatement and proof · cited by 113
- top_uniqueproof · cited by 102
Cited by1
Results whose statement or proof uses this declaration.
- DFinsupp.addHom_extproof · cited by 4