Commit 2025-06-24 10:56 367d0c61
View on Github →refactor: move the definition of IsRegular earlier (#26321)
The motivation here is to be able to define things like IsCancelMulZero in terms of IsRegular, which would allow API for the latter to be used to provide instances for the former.
As a first step, this moves the MulZeroClass lemmas abut IsRegular into the GroupWithZero folder, which is consistent with the ring lemmas living inside the Ring folder.