Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_one_le_two_mul

Modification history

2022-04-02 11:56

src/algebra/order/ring.lean

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

Modified add_one_le_two_mul View on Github →

2021-06-20 21:36

src/algebra/ordered_ring.lean

feat(algebra/ordered_ring): `a + 1 ≤ 2 * a` (#7995) …

Added add_one_le_two_mul View on Github →