Theorem List.getD_surjective

Modification history

2025-11-05 02:43
Mathlib/Data/List/GetD.lean
feat(Data/List/GetD): `getD` is surjective iff every element is in the list (#30217)
Added List.getD_surjectiveView on Github →