refactor(algebra/monoid_algebra/{ basic + support } + import dust): move lemmas to a new "support" file (#16322)
This PR moves some lemmas from `algebra/monoid_algebra/basic` to the new file `algebra/monoid_algebra/support`.
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/splitting.20support.20from.20algebra.2Fmonoid_algebra.2Fbasic)