Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-01 10:46 e6a0a266

View on Github →

chore(algebra/order/*): generalisation linter (#13098)

Estimated changes

modified theorem with_bot.add_bot
modified theorem with_bot.add_eq_bot
modified theorem with_bot.bot_add
modified theorem with_bot.coe_add
modified theorem with_bot.coe_bit0
modified theorem with_bot.coe_bit1
modified theorem with_zero.coe_le_coe
modified theorem with_zero.coe_lt_coe
modified theorem mul_left_cancel''
modified theorem mul_right_cancel''