Def Bundle.ContMDiffRiemannianMetric.toRiemannianMetric

Modification history

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