Theorem min_mul

Modification history

2025-08-13 11:43

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

chore(Algebra/Order): replace Co/ContravariantClass by established abbrevs (#28239) …

Modified min_mul View on Github →

2024-12-05 08:47

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

feat: add `mul_min` and `min_mul` (#18926)

Added min_mul View on Github →