Theorem mul_add_mul_le_mul_add_mul'

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_add_mul_le_mul_add_mul'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_add_mul_le_mul_add_mul'View on Github →

2024-01-01 07:00

Mathlib/Algebra/Order/Ring/Canonical.lean

chore: Generalise monotonicity of multiplication lemmas to semirings (#9369) …

Modified mul_add_mul_le_mul_add_mul'View on Github →

2023-01-19 10:36

Mathlib/Algebra/Order/Ring/Canonical.lean

chore: format by line breaks with long lines (#1529) …

Modified mul_add_mul_le_mul_add_mul'View on Github →

2022-12-08 07:28

Mathlib/Algebra/Order/Ring/Canonical.lean

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

Added mul_add_mul_le_mul_add_mul'View on Github →