mathlib

ad84a13c - feat(analysis/calculus/fderiv/star): derivative of star in star-modules over a trivial star-ring (#19038)

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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Star-semilinear.20maps.20are.20semilinear.20when.20star.20is.20trivial/near/359552581). 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.