Mathlib v3 is deprecated. Go to Mathlib v4

Def function.embedding.inr

Modification history

2021-01-27 08:41
src/logic/embedding.lean
chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888) …
Modified function.embedding.inrView on Github →
2020-06-11 18:53
src/logic/embedding.lean
feat(*): preparations for Caratheodory's convexity theorem (#3030)
Added function.embedding.inrView on Github →