# Commit 2023-05-23 12:33 ad84a13c

View 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 `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.