Commit 2023-05-23 12:33 ad84a13cView on Github →
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
Some alternative approaches are discussed on Zulip.
These API here is just the API for
neg), modified by replacing
-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.