Theorem Prod.Lex.prodUnique_apply

Modification history

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