Theorem Option.getD_comp_some

Modification history

2025-11-20 14:55
Mathlib/Data/Option/Basic.lean
feat: add `getD_comp_some` lemma for `Option` type (#31828) …
Added Option.getD_comp_someView on Github →