Theorem Prod.mk_inj_right

Modification history

2024-04-14 10:41

Mathlib/Data/Prod/Basic.lean

chore: remove autoImplicit from more files (#11798) …

Modified Prod.mk_inj_right View on Github →

2022-12-14 10:48

Mathlib/Data/Prod/Basic.lean

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

Added Prod.mk_inj_right View on Github →