Def Bundle.ContinuousRiemannianMetric.toRiemannianMetric

Modification history

2025-06-24 13:20

Mathlib/Topology/VectorBundle/Riemannian.lean

feat: continuous Riemannian vector bundles (#26197) …

Added Bundle.ContinuousRiemannianMetric.toRiemannianMetric View on Github →