feat(algebra/algebra/*): generalise (#13252)
Some generalisations straight from Alex's generalisation linter, with some care about how to place them. Some `algebra` lemmas are weakened to semirings, allowing us to talk about ℕ-algebras much more easily.
