Theorem Prod.mk_inj_right

Modification history

2025-03-07 13:46
Mathlib/Data/Prod/Basic.lean
chore: rename injectivity of `Prod.mk` lemmas (#22634) …
Deleted Prod.mk_inj_rightView on Github →
2024-04-14 10:41
Mathlib/Data/Prod/Basic.lean
chore: remove autoImplicit from more files (#11798) …
Modified Prod.mk_inj_rightView on Github →
2022-12-14 10:48
Mathlib/Data/Prod/Basic.lean
feat: `prod.lex` is trichotomous (#989) …
Added Prod.mk_inj_rightView on Github →