Commit 2022-12-23 02:51 3bc62129

View on Github →

refactor: use Is*CancelMulZero (#1137) This is a Lean 4 version of leanprover-community/mathlib#17963

Estimated changes

Modified Mathlib/Algebra/Associated.lean

deleted theorem Associates.eq_of_mul_eq_mul_left

deleted theorem Associates.eq_of_mul_eq_mul_right

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

deleted theorem CommMonoidWithZero.IsLeftCancelMulZero.to_IsCancelMulZero

deleted theorem CommMonoidWithZero.IsLeftCancelMulZero.to_IsRightCancelMulZero

deleted theorem CommMonoidWithZero.IsRightCancelMulZero.to_IsCancelMulZero

deleted theorem CommMonoidWithZero.IsRightCancelMulZero.to_IsLeftCancelMulZero

added theorem IsLeftCancelMulZero.to_IsCancelMulZero

added theorem IsLeftCancelMulZero.to_IsRightCancelMulZero

added theorem IsRightCancelMulZero.to_IsCancelMulZero

added theorem IsRightCancelMulZero.to_IsLeftCancelMulZero

Modified Mathlib/Algebra/Ring/Regular.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Nat/Choose/Basic.lean