Fix build by removing references to missing artefacts

leanprover-community / sphere-eversion

Formalization of the existence of sphere eversions

Apache License 2.0

36 stars 10 forks source link

Closed ocfnash closed 2 years ago

ocfnash commented 2 years ago

Specifically:

the lemma linear_map.ker_to_continuous_linear_map no longer exists
the file to_mathlib.analysis.normed_space.finite_dimension.lean no longer exists

ocfnash commented 2 years ago