Theorem List.get?_injective

Modification history

2024-05-05 03:48

Mathlib/Data/List/Basic.lean

chore: deprecate redundant lemma List.get?_injective (#12630) …

Deleted List.get?_injective View on Github →

2023-01-05 14:40

Mathlib/Data/List/Basic.lean

feat port: Data.List.Basic (#966) …

Modified List.get?_injective View on Github →

2021-12-18 19:21

Mathlib/Data/List/Basic.lean

feat: porting Data.List.Defs, Init.Data.List.Basic (#137) …

Added List.get?_injective View on Github →