Theorem Prod.Lex.lt_iff'

Modification history

2025-01-22 11:38
Mathlib/Data/Prod/Lex.lean
feat: definition of `<` on `α ×ₗ β` in partial orders (#20067) …
Added Prod.Lex.lt_iff'View on Github →