sphere-eversion
sphere-eversion copied to clipboard
chore: use new elaborators more
- depends on: mathlib4#30413
- further use will need
- a fix in the elaborators: if E is a real inner product space, we don't find the trivial model yet (even though InnerProductSpace implies NormedSpace)
- an extension for finding the model on OneJetBundle... perhaps when this is an environment extension, so can be don here also