Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.mk_inj_right

Modification history

2022-12-14 05:27

src/data/prod/basic.lean

feat(data/prod/basic): `prod.lex` is trichotomous (#17931) …

Added prod.mk_inj_right View on Github →