Theorem IsMax.prod_mk

Modification history

2025-02-25 19:33

Mathlib/Order/Max.lean

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

Deleted IsMax.prod_mk View on Github →

2022-11-18 04:15

Mathlib/Order/Max.lean

feat: port Order.Max (#567) …

Added IsMax.prod_mk View on Github →