OAI/Geometry/RCD/Harmonic/AffinePathDerivative.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The interior derivative of an affine coordinate path
- theorem
OAI.RegularPointCoordinates.affine_path_hasDerivAtline 12