Commit 2023-11-15 19:17 0b128365
View on Github →feat: non-zero smul-divisors (#7138) If $R$ is a monoid with $0$ and $M$ an additive monoid with an $R$-action, then the set of non-zero smul-divisors of $R$ is a submonoid. for any $r \in R$, $r$ is a non-zero smul-divisors if and only if for any $m\in M$, $r \cdot m = 0$ implies $m = 0$. These elements are also called $M$-regular. They are useful in regular sequences.