Theorem List.getD_replicate

Modification history

2025-12-08 14:02

Mathlib/Data/List/GetD.lean

feat(Data/List/GetD): golf and add lemmas for `get` and `getElem?` (#30213)

Modified List.getD_replicate View on Github →

2024-12-03 19:01

Mathlib/Data/List/GetD.lean

feat: `List.destutter` on cotransitive relations. (#9082) …

Added List.getD_replicate View on Github →