Def Prod.Lex.prodUnique

Modification history

2025-07-05 03:31
Mathlib/Order/Hom/Lex.lean
feat(Order): orderIso for degenerate Lex prod (#26773)
Added Prod.Lex.prodUniqueView on Github →