Theorem Prod.lex_iff

Modification history

2024-10-04 03:33

Mathlib/Data/Prod/Basic.lean

chore: bump toolchain to v4.13.0-rc2 (#17377) …

Modified Prod.lex_iff View on Github →

2022-12-14 10:48

Mathlib/Data/Prod/Basic.lean

feat: `prod.lex` is trichotomous (#989) …

Added Prod.lex_iff View on Github →