Theorem Prod.Lex.toLex_ge_toLex

Modification history

2026-10-04 06:22
Mathlib/Order/Prod/Lex/Basic.lean
feat(Translate): command for adding a translation (#43750) …
Deleted Prod.Lex.toLex_ge_toLexView on Github →
2026-04-21 17:27
Mathlib/Data/Prod/Lex.lean
chore(Data/Prod/Lex): use `to_dual` (#38196)
Added Prod.Lex.toLex_ge_toLexView on Github →