Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-04-21 17:27
1eddfcd2
View on Github →
chore(Data/Prod/Lex): use
to_dual
(
#38196
)
Estimated changes
Modified
Mathlib/Data/Prod/Lex.lean
added
theorem
Prod.Lex.toLex_ge_toLex
added
theorem
Prod.Lex.toLex_gt_toLex