mathlib

ffcdedba - remove complete_space assumption in lemmas