Theorem smul_mem_nonZeroDivisorsRight

Modification history

2026-10-10 12:26
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
feat(Algebra.GroupWithZero): generalize SMulZeroClass to MonoidWithZero and lift MulDistribMulAction to nonZeroDivisors (#40604) …
Added smul_mem_nonZeroDivisorsRightView on Github →