feat(algebra/monoid_algebra): add division by a generator (#15905)
This generalizes `polynomial.div_X`.
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/X_i.20divides.20f.20if.20f.3D0.20when.20X_i.3D0/near/339570367)