Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-14 05:27 198161d8

View on Github →

feat(data/prod/basic): prod.lex is trichotomous (#17931) or irreflexive when the base relations are.

Estimated changes

added theorem prod.lex_iff
modified theorem prod.mk.inj_iff
added theorem prod.mk_inj_left
added theorem prod.mk_inj_right