Commit 2024-07-06 12:37 139bf21f

View on Github →

feat: min_mul_min_le_min_mul_mul (#14476)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Defs.lean

added theorem min_mul_min_le_mul_min_min