Theorem mul_le_mul_of_nonpos_of_nonpos'

Modification history

2024-07-31 01:56

Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

chore (Algebra.Order.Ring.Unbundled.Basic): inline typeclass assumptions (#15334) …

Modified mul_le_mul_of_nonpos_of_nonpos'View on Github →

2024-07-16 22:43

Mathlib/Algebra/Order/Ring/Defs.lean

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

Modified mul_le_mul_of_nonpos_of_nonpos'View on Github →

2022-12-08 07:28

Mathlib/Algebra/Order/Ring/Defs.lean

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

Added mul_le_mul_of_nonpos_of_nonpos'View on Github →