Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-21 21:36 a47cda96

View on Github →

refactor(algebra/group_with_zero/defs): use is_*cancel_mul_zero (#17963)

Estimated changes

Modified archive/imo/imo1988_q6.lean

Modified src/algebra/associated.lean

deleted theorem associates.eq_of_mul_eq_mul_left

deleted theorem associates.eq_of_mul_eq_mul_right

Modified src/algebra/char_p/basic.lean

Modified src/algebra/group_with_zero/defs.lean

deleted theorem comm_monoid_with_zero.is_left_cancel_mul_zero.to_is_cancel_mul_zero

deleted theorem comm_monoid_with_zero.is_left_cancel_mul_zero.to_is_right_cancel_mul_zero

deleted theorem comm_monoid_with_zero.is_right_cancel_mul_zero.to_is_cancel_mul_zero

deleted theorem comm_monoid_with_zero.is_right_cancel_mul_zero.to_is_left_cancel_mul_zero

added theorem is_left_cancel_mul_zero.to_is_cancel_mul_zero

added theorem is_left_cancel_mul_zero.to_is_right_cancel_mul_zero

added theorem is_right_cancel_mul_zero.to_is_cancel_mul_zero

added theorem is_right_cancel_mul_zero.to_is_left_cancel_mul_zero

Modified src/algebra/ring/regular.lean

Modified src/data/nat/basic.lean

deleted theorem nat.eq_of_mul_eq_mul_right

Modified src/data/nat/choose/basic.lean

Modified src/data/nat/gcd/basic.lean

Modified src/data/rat/defs.lean

Modified src/number_theory/cyclotomic/primitive_roots.lean

Modified src/number_theory/zsqrtd/basic.lean

Modified src/ring_theory/localization/fraction_ring.lean

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/valuation/valuation_ring.lean