Theorem Option.getD_coe

Modification history

2023-07-21 22:53

Mathlib/Data/Option/Basic.lean

chore(Data/Option): add 3 missing lemmas and some `align`s (#6049) …

Deleted Option.getD_coe View on Github →

2022-11-07 03:58

Mathlib/Data/Option/Basic.lean

feat: port Data.Option.Basic (#493) …

Added Option.getD_coe View on Github →