Commit 2026-10-10 12:26 48026013

feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors (#40604) Generalize the instance SMulZeroClass α β under [Group α] [GroupWithZero β] [MulDistribMulAction α β]to [Group α] [MonoidWithZero β] [MulDistribMulAction α β]. From an action [Group G] [MonoidWithZero M] [MulDistribMulAction G M], use this instance to construct an action on the nonzero divisors of M. No diamond: there is no general instance giving an action on a submonoid as a target (that would need the submonoid to be invariant, which isn't automatic), so defining the action on nonZeroDivisors should not clash with anything . :robot: This PR was extracted from the SKW project by Claude.