feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors#40604

Open

xroblot wants to merge 8 commits into

leanprover-community:masterfrom

xroblot:feat/MulDistribMulAction-smul-zero

Commits on Jun 14, 2026

feat(Algebra.GroupWithZero.Action.Defs): generalize SMulZeroClass instance from GroupWithZero to MonoidWithZero
xroblot
committed
feat(Algebra.GroupWithZero): group acting via MulDistribMulAction sends zero to zero; lift to nonZeroDivisors
xroblot
committed

Commits on Jun 18, 2026

Merge remote-tracking branch 'upstream/master' into feat/MulDistribMulAction-smul-zero
xroblot
committed

Commits on Jun 19, 2026

Commits on Jun 21, 2026

clean up + golf
xroblot
committed

Commits on Jul 18, 2026

Merge branch 'master' into feat/MulDistribMulAction-smul-zero
xroblot
authored

Commits on Jul 23, 2026

Merge branch 'master' into feat/MulDistribMulAction-smul-zero
themathqueen
authored