Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-12 09:03 3afdf41f

View on Github →

chore(*): generalize some lemmas from linear_ordered_semiring to ordered_semiring (#5327) API changes:

  • Many lemmas now have weaker typeclass assumptions. Sometimes this means that @myname _ _ _ needs one more _.
  • Drop eq_one_of_mul_self_left_cancel etc in favor of the new mul_eq_left_iff etc.
  • A few new lemmas that state monotone or strict_mono_incr_on.

Estimated changes

modified theorem exists_nat_ge
modified theorem exists_nat_gt
modified theorem two_ne_zero'
added theorem left_eq_mul_iff
added theorem mul_eq_left_iff
added theorem mul_eq_right_iff
added theorem right_eq_mul_iff
added theorem pow_mono
added theorem strict_mono_pow
modified theorem int.cast_abs
modified theorem int.cast_le
modified theorem int.cast_lt
modified theorem int.cast_lt_zero
modified theorem int.cast_max
modified theorem int.cast_min
added theorem int.cast_mono
modified theorem int.cast_nonneg
modified theorem int.cast_nonpos
modified theorem int.cast_pos
added theorem int.cast_strict_mono
modified theorem nat.abs_cast
modified theorem nat.cast_add_one_pos
modified theorem nat.cast_le
modified theorem nat.cast_le_one
modified theorem nat.cast_lt
modified theorem nat.cast_lt_one
modified theorem nat.cast_nonneg
modified theorem nat.cast_pos
modified theorem nat.cast_two
added theorem nat.mono_cast
modified theorem nat.one_le_cast
modified theorem nat.one_lt_cast
modified theorem nat.strict_mono_cast
modified theorem tendsto_coe_int_at_top_iff
modified theorem tendsto_coe_nat_at_top_iff