A variant of Nat that has instance Zero to return 1?

Stream: Is there code for X?

[Siddharth Bhat]

I want to use Finsupp α ℕ, where the default value of the Finsupp where the support does not exist is considered to be 1 (and the additive monoid to be considered as multiplication, of course). How exactly should I achieve this? I can't imagine I'm the first one to want this!

[Eric Wieser]

Finsupp α (Additive ℕ) will work

[Eric Wieser]

Multiplicative (Finsupp α (Additive ℕ)) might be nicer, since 1 is the constant function of all 1s

[Yaël Dillies]

@Sky Wilshaw was thinking about this

[Sky Wilshaw]

I was working on a PR to add another parameter to finsupp but that was back in the mathlib3 days, I unfortunately never got round to it