Def Bundle.ContMDiffRiemannianMetric.toContinuousRiemannianMetric

Modification history

2025-07-04 20:03
Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean
feat: smooth Riemannian bundles (#26506) …
Added Bundle.ContMDiffRiemannianMetric.toContinuousRiemannianMetricView on Github →