Commit 2024-09-12 10:52 dc64441f

feat: Prop-valued version of RCLike structure for normed fields (#16383) Motivation: I want a typeclass to be able to say that some classes of functions have symmetric second derivative wrt some normed field (this is a key point when defining the Lie algebra of a Lie group). Over R or C, this is true for C^2 functions. Over a general field, this is true for analytic functions. A first step is to have a typeclass saying whether a given normed field is R or C, implemented in this PR.