Theorem Sum.elim_injective

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 Sum.elim_injective View on Github →

2025-05-15 08:57

Mathlib/Data/Sum/Basic.lean

feat: `Iff` version of `Injective.sumElim` (#24899) …

Added Sum.elim_injective View on Github →