Theorem Prod.lex_iff

Modification history

2022-12-14 10:48
Mathlib/Data/Prod/Basic.lean
feat: `prod.lex` is trichotomous (#989) …
Added Prod.lex_iffView on Github →