Theorem monotone_prod_iff

Modification history

2025-02-18 13:54
Mathlib/Order/Monotone/Basic.lean
chore(Order/Monotone): split `Basic.lean` into `Basic.lean` and `Defs.lean` (#22004) …
Modified monotone_prod_iffView on Github →
2025-02-03 11:03
Mathlib/Order/Monotone/Basic.lean
feature(Order/Monotone/Basic): Separately monotone iff jointly monotone (#20254) …
Added monotone_prod_iffView on Github →