Documentation

SpherePacking.ForMathlib.MDifferentiableFunProp

fun_prop Lemmas for Manifold Differentiability #

fun_prop lemmas for manifold differentiability of functions on the upper half-plane.