Theorem Prod.GCongr.mk_le_mk

Modification history

2025-12-02 12:55
Mathlib/Order/Basic.lean
chore(Order/Basic): use `@[to_dual]` (#31903) …
Modified Prod.GCongr.mk_le_mkView on Github →
2025-05-29 18:50
Mathlib/Order/Basic.lean
feat(Order): add gcongr lemmas for Prod.mk (#25301) …
Added Prod.GCongr.mk_le_mkView on Github →