`OAI/Geometry/RCD/Harmonic/FirstOrderAbsoluteAffineMean.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mean absolute affine defects of the original splitting coordinates

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.first_order_absolute_affine_mean line 15