Commit 2022-11-30 13:42 3a3b30d1

View on Github →

feat: add IsCancelMulZero (#724) We add IsCancelMulZero and related classes. This is the continuation of [#606](https://github.com/leanprover-community/mathlib4/pull/606). Corresponding mathlib3 PR [#17716](https://github.com/leanprover-community/mathlib/pull/17716).

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

added theorem CommMonoidWithZero.IsLeftCancelMulZero.to_IsCancelMulZero

added theorem CommMonoidWithZero.IsLeftCancelMulZero.to_IsRightCancelMulZero

added theorem CommMonoidWithZero.IsRightCancelMulZero.to_IsCancelMulZero

added theorem CommMonoidWithZero.IsRightCancelMulZero.to_IsLeftCancelMulZero