OAI/Geometry/RCD/Sobolev/HessianActionRepresentatives.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transferring Hessian actions between locally equal directions

  1. theorem OAI.RegularPointCoordinates.localHessianAction_congr_of_grams line 13