Theorem Prod.Lex.uniqueProd_apply

Modification history

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