Commit 2023-11-03 14:01 36d79494

feat: finite-dimensional manifolds are locally compact (#7822) ... assuming they're modelled over a locally compact field. (Currently, the only such instances in mathlib are $\mathbb{R}$ and $\mathbb{C}$. Once local compactness of the $p$-adic numbers is added to mathlib, this theorem will apply to them also.)

• part of the road towards Sard's theorem