splitting support from algebra/monoid_algebra/basic

Stream: general

[Damiano Testa]

Dear All,

I find algebra/monoid_algebra/basic way too big and slow. Moreover, I am planning to add more lemmas about the support of elements in add_monoid_algebras. Rather than adding more lemmas to this already very large file, I am thinking of splitting off lemmas that specifically talk about the support to a new file.

It turns out that this removes very few lemmas from the big file, but at least it is a step in what I consider to be the right direction!

Anyone has any opinion?

[Damiano Testa]

If you want to take a look at the current split, I am trying it in #16322.