Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sum.injective_inr

Modification history

2021-03-18 19:27
src/data/sum.lean
chore(*): update `injective` lemma names to match the naming guide (#6740) …
Deleted sum.injective_inrView on Github →
2020-10-11 16:27
src/data/sum.lean
chore(*): assorted lemmas (#4566) …
Added sum.injective_inrView on Github →