Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 04:12 428acaae

View on Github →

move(algebra/order/monoid/*): relocate zero_le_one_class again (#17820) #17646 move zero_le_one_class to algebra.order.monoid.with_zero. This PR split things about zero_le_one_class into two files. Also, all lemmas about numerics other than 0 and 1 require typeclass add_monoid_with_one now. Zulip

Estimated changes

added theorem lt_add_one
added theorem lt_one_add
added theorem one_le_two'
added theorem one_le_two
added theorem one_lt_two
added theorem zero_le_four
added theorem zero_le_three
added theorem zero_le_two
added theorem zero_lt_four'
added theorem zero_lt_four
added theorem zero_lt_three'
added theorem zero_lt_three
added theorem zero_lt_two'
added theorem zero_lt_two
deleted theorem lt_add_one
deleted theorem lt_one_add
deleted theorem one_le_two'
deleted theorem one_le_two
deleted theorem one_lt_two
deleted theorem zero_le_four
deleted theorem zero_le_one'
deleted theorem zero_le_one
deleted theorem zero_le_three
deleted theorem zero_le_two
deleted theorem zero_lt_four'
deleted theorem zero_lt_four
deleted theorem zero_lt_one'
deleted theorem zero_lt_one
deleted theorem zero_lt_three'
deleted theorem zero_lt_three
deleted theorem zero_lt_two'
deleted theorem zero_lt_two
added theorem zero_le_one'
added theorem zero_le_one
added theorem zero_lt_one'
added theorem zero_lt_one