Derivative commutes with conjugation

Stream: Is there code for X?

[Eric Wieser]

Am I blind, or do we really not have $\frac{d}{dr}(f(r)^*) = \frac{df}{dr}^*$ for $f : \mathbb{R} \to \mathbb{C}$? Searching for deriv conj or deriv star in the docs doesn't find anything

[Anatole Dedecker]

I can't find it, but you should be able to apply docs#continuous_linear_map.has_fderiv_at to docs#starₗᵢ to get there (although in theory we don't need a norm for that, we should have a starL assuming docs#has_continuous_star instead of docs#normed_star_group)

[Eric Wieser]

#19037 adds starL

[Eric Wieser]

#19038 adds the fderiv results (and depends on the above)