Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 08:49 186660c0

View on Github →

feat(*): assorted simp lemmas for IMO 2019 q1 (#4383)

  • mark some lemmas about cancelling in expressions with (-) as simp;
  • simplify a * b = a * c to b = c ∨ a = 0, and similarly for `a * c = b * c;
  • change priority of monoid.has_pow and group.has_pow to the default priority.
  • simplify monoid.pow and group.gpow to has_pow.pow.

Estimated changes

modified theorem add_add_neg_cancel'_right
modified theorem add_add_sub_cancel
modified theorem add_sub_sub_cancel
modified theorem sub_add_add_cancel
modified theorem sub_add_sub_cancel'
modified theorem sub_sub_cancel
modified theorem sub_sub_sub_cancel_left
added theorem inv_mul_cancel_comm
added theorem mul_inv_cancel_comm
added theorem group.gpow_eq_has_pow
added theorem monoid.pow_eq_has_pow
added theorem mul_eq_mul_left_iff
added theorem mul_eq_mul_right_iff
deleted theorem padic_int.cast_pow
added theorem padic_int.coet_pow