don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
theory Multivariate_Analysisimports Ordered_Euclidean_Space Determinants Cross3 Lipschitz Starlikebegintext \<open>Entry point excluding integration and complex analysis.\<close>end