Theorem IsCovariantDerivativeOn.torsion_apply_eq_extend

Modification history

2026-03-18 22:42
Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Torsion.lean
feat: torsion of an affine connection (#36285) …
Added IsCovariantDerivativeOn.torsion_apply_eq_extendView on Github →