Theorem List.getD_eq_getElem?

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)
Added List.getD_eq_getElem?View on Github →