port-complete
default avatar
wieser.eric@gmail.com
46f71c61 · chore(Data/Option): add 3 missing lemmas and some `align`s (#6049) · 
This commit is the last that is guaranteed to be synchronized with mathlib3