Def Finsupp.single

Modification history

2024-05-17 19:31

Mathlib/Data/Finsupp/Defs.lean

style: remove all isolated `where` (#12991)

Modified Finsupp.single View on Github →

2023-01-27 13:32

Mathlib/Data/Finsupp/Defs.lean

feat: port Data.Finsupp.Defs (#1807)

Added Finsupp.single View on Github →