Structure Bundle.ContinuousRiemannianMetric

Modification history

2025-06-24 13:20
Mathlib/Topology/VectorBundle/Riemannian.lean
feat: continuous Riemannian vector bundles (#26197) …
Added Bundle.ContinuousRiemannianMetricView on Github →