Theorems · Theorem · general algebraic systems
Finsupp.toDFinsupp_single
∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] (i : ι) (m : M),
(fun₀ | i => m).toDFinsupp = fun₀ | i => m- Defined in
- Mathlib.Data.Finsupp.ToDFinsupp
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsupp.singlestatement · cited by 943
- DFinsuppstatement · cited by 694
- DFinsupp.singlestatement · cited by 113
- Finsupp.single_applyproof · cited by 99
- DFinsupp.extproof · cited by 78
- DFinsupp.single_applyproof · cited by 35
- Finsupp.toDFinsuppstatement · cited by 21
Cited by10
Results whose statement or proof uses this declaration.
- finsuppLEquivDirectSum_singleproof · cited by 4
- MultilinearMap.freeFinsuppEquiv_singleproof · cited by 2
- PiTensorProduct.ofFinsuppEquiv_tprod_singleproof · cited by 2
- AddMonoidAlgebra.toDirectSum_singleproof · cited by 1
- lsum_comp_mapRange_toSpanSingletonproof · cited by 1
- AddMonoidAlgebra.toDirectSum_intCastproof · cited by 0
- AddMonoidAlgebra.toDirectSum_natCastproof · cited by 0
- Module.Presentation.finsupp_varproof · cited by 0
- AddMonoidAlgebra.toDirectSum_ofNatproof · cited by 0
- AddMonoidAlgebra.toDirectSum_oneproof · cited by 0