Commit 2023-07-21 22:53 46f71c61

View on Github →

chore(Data/Option): add 3 missing lemmas and some aligns (#6049) The lemmas were lost while porting. Also drop Option.getD_coe since it is the same as Option.getD_some.

Estimated changes

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.exists_mem_map

added theorem Option.forall_mem_map

deleted theorem Option.getD_coe

added theorem Option.mem_map

Modified Mathlib/Data/Polynomial/Degree/TrailingDegree.lean

Modified Mathlib/Init/Data/Option/Lemmas.lean