Theorem Function.Injective.sumElim

Modification history

2025-05-16 03:37
Mathlib/Data/Sum/Basic.lean
feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types (#24167) …
Modified Function.Injective.sumElimView on Github →
2025-02-20 18:07
Mathlib/Data/Sum/Basic.lean
chore: rename Injective.sum_elim and friends (#22129) …
Added Function.Injective.sumElimView on Github →