Commit 2023-05-23 12:33 ad84a13c

feat(analysis/calculus/fderiv/star): derivative of star in star-modules over a trivial star-ring (#19038) Notably this includes the complex and quaternion conjugates. We need the has_trivial_star assumption in order to have star (c • x) = c • star x available; which in turn we need because has_fderiv_at consumes linear maps not semi-linear maps. In the absence of an easy way to convert between linear and semi-linear maps, we bundle star (again) as a continuous linear equiv as starL'. Some alternative approaches are discussed on Zulip. These API here is just the API for - (neg), modified by replacing neg with star and -f x with star (f x). Since we require has_trivial_star there is no point adding any lemmas for the derivative of star on the field itself.