Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-03 22:00 c4bf9e44

View on Github →

chore(algebra/ordered_group): deduplicate (#3279) For historical reasons we have some lemmas duplicated for ordered_comm_monoid and ordered_cancel_comm_monoid. This PR merges some duplicates.

Estimated changes

deleted theorem le_mul_of_le_of_one_le'
deleted theorem le_mul_of_one_le_left''
deleted theorem le_mul_of_one_le_of_le'
deleted theorem le_mul_of_one_le_right''
deleted theorem lt_of_mul_lt_mul_left''
deleted theorem lt_of_mul_lt_mul_right''
deleted theorem mul_le_mul_left''
modified theorem mul_le_mul_left'
deleted theorem mul_le_mul_right''
modified theorem mul_le_mul_right'
deleted theorem mul_le_one''
deleted theorem mul_one_lt'
deleted theorem mul_one_lt
deleted theorem one_le_mul'
added theorem one_lt_mul'
modified theorem filter.tendsto_at_top_mono'