Commit 2025-07-05 03:31 0d153f6e

View on Github →

feat(Order): orderIso for degenerate Lex prod (#26773)

Estimated changes

Modified Mathlib/Order/Hom/Lex.lean

added def Prod.Lex.prodUnique

added theorem Prod.Lex.prodUnique_apply

added def Prod.Lex.uniqueProd

added theorem Prod.Lex.uniqueProd_apply