Theorem nonZeroDivisors.val_smul

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 nonZeroDivisors.val_smulView on Github →