multiset: smul vs nsmul

Stream: general

[Ruben Van de Velde]

docs#multiset seems to refer to •ℕ both as "smul" and "nsmul" - card_smul/count_smul/prod_smul vs map_nsmul/mem_nsmul. Should those be consistent?

[Eric Wieser]

If it uses that symbol it should be called nsmul

[Eric Wieser]

docs#nsmul_eq_smul relates the two

[Mario Carneiro]

Well, multiset isn't a nat semimodule I think

[Mario Carneiro]

The *_smul lemmas date back before the \N was part of the syntax

[Mario Carneiro]

I'd personally be okay with calling it all smul since there is no disambiguation to be had

[Yury G. Kudryashov]

Well, multiset isn't a nat semimodule I think

It's an additive commutative monoid, so it is a nat semimodule.

[Mario Carneiro]

Ah. Well I think it shouldn't be, re: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finsupp.2Ehas_scalar/near/230579612

[Eric Wieser]

Mario Carneiro said:

I'd personally be okay with calling it all smul since there is no disambiguation to be had

smul and nsmul are only defeq if you're using docs#add_monoid_hom.nat_semimodule. If you're using any other module structure, you need docs#nsmul_eq_smul to rewrite between them. The chance of the user finding that lemma is a lot lower if we call •ℕ smul elsewhere.