Def Prod.Lex.uniqueProd

Modification history

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