Theorem IsMax.prodMk

Modification history

2025-12-03 01:23

Mathlib/Order/Max.lean

feat(Order/Max): use `@[to_dual]` (#32059) …

Deleted IsMax.prodMk View on Github →

2025-02-25 19:33

Mathlib/Order/Max.lean

chore(Order/Max): rename `prod_mk` -> `prodMk` (#22188)

Added IsMax.prodMk View on Github →