Commit 2025-12-08 14:02 cc32bd18

View on Github →

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

Estimated changes

Modified Mathlib/Data/List/GetD.lean

added theorem List.getD_eq_get

deleted theorem List.getD_eq_getD_getElem?

added theorem List.getD_eq_getElem?

modified theorem List.getD_map

modified theorem List.getD_replicate

modified theorem List.getElem?_getD_singleton_default_eq