Commit 2025-08-02 22:46 d0323fbd

View on Github →

chore(Algebra/Regular): split Defs out of Basic and redefine IsCancelMul (#27791) Redefine Is(Left/Right)CancelMul(Zero) in terms of Is(Left/Right)Regular. Defeq to the original defs except for argument explicitness/order. Part of #22997

Estimated changes

added theorem IsLeftRegular.all
added theorem IsRegular.all
added theorem IsRightRegular.all
modified theorem Commute.isRightRegular_iff
deleted structure IsAddRegular
deleted theorem IsLeftRegular.all
deleted def IsLeftRegular
deleted theorem IsRegular.all
modified theorem IsRegular.pow
modified theorem IsRegular.pow_iff
deleted structure IsRegular
deleted theorem IsRightRegular.all
deleted def IsRightRegular
deleted theorem isRegular_iff
added structure IsAddRegular
added def IsLeftRegular
added structure IsRegular
added def IsRightRegular
added theorem isRegular_iff