Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.lex_iff

Modification history

2022-12-14 05:27
src/data/prod/basic.lean
feat(data/prod/basic): `prod.lex` is trichotomous (#17931) …
Added prod.lex_iffView on Github →