Theorem add_one_le_two_mul

Modification history

2024-07-16 22:43

Mathlib/Algebra/Order/Ring/Defs.lean

chore (Algebra.Order.Ring.Defs): split file and unbundle results (#14393) …

Modified add_one_le_two_mul View on Github →

2022-12-08 07:28

Mathlib/Algebra/Order/Ring/Defs.lean

feat: port Algebra.Order.[Ring|Field].Defs (#905) …

Added add_one_le_two_mul View on Github →