Commit 2022-12-14 10:48 3db783cf

View on Github →

feat: prod.lex is trichotomous (#989) Match https://github.com/leanprover-community/mathlib/pull/17931

Estimated changes

Modified Mathlib/Data/Prod/Basic.lean

added theorem Prod.lex_iff

added theorem Prod.mk_inj_left

added theorem Prod.mk_inj_right