Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-02 11:56 7df59077

View on Github →

chore(algebra/order/ring): generalisation linter (#13096)

Estimated changes

modified theorem add_one_le_two_mul
modified theorem with_bot.bot_lt_mul
modified theorem with_top.mul_lt_top