Def CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover

Modification history

2026-07-27 17:36
Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean
chore(Geometry/Manifold): fix defs with underscores (#42115) …
Deleted CovariantDerivative.of_isCovariantDerivativeOn_of_open_coverView on Github →
2026-03-12 19:24
Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean
feat: covariant derivatives on vector bundles (#36279) …
Added CovariantDerivative.of_isCovariantDerivativeOn_of_open_coverView on Github →