Commit 2025-09-18 17:55 a56c0075

View on Github →

fix: riemmanian -> riemannian (#28581) changed riemmanian to riemannian

Estimated changes

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

added theorem eventually_riemannianEDist_lt

deleted theorem eventually_riemmanianEDist_lt

added theorem setOf_riemannianEDist_lt_subset_nhds'

added theorem setOf_riemannianEDist_lt_subset_nhds

deleted theorem setOf_riemmanianEDist_lt_subset_nhds'

deleted theorem setOf_riemmanianEDist_lt_subset_nhds