First PR: derivative and complex conjugate

Stream: new members

[Evan O'Dorney]

Greetings, all! I am a postdoc in number theory and have been learning Lean for the past three weeks. I have been contributing to the Prime Number Theorem formalization project and am contributing my first Mathlib PR, a lemma in complex analysis that I expect will be useful to others: if $f : \mathbb{C} \to \mathbb{C}$ is a function, the derivative of $\operatorname{conj} \circ f \circ \operatorname{conj}$ is $\operatorname{conj} \circ f' \circ \operatorname{conj}$, where $\operatorname{conj}$ denotes complex conjugation. Please let me know how I can improve my draft PR.

[Kenny Lau]

Welcome to Mathlib!

[Kenny Lau]

@Evan O'Dorney Thanks for the addition! I've golfed some of your code so that the proofs look cleaner.

[Kenny Lau]

btw I would make it not a draft ASAP so that more people will review it

[Michael Rothgang]

Welcome! It's great to have new people around, and already making a mathlib PR after three weeks is impressive!
I have labelled your PR awaiting-author: once you have addressed Kenny's comments, just remove this label (and undraft your PR); the reviewers will know it is ready for another look.

[Eric Wieser]

I think @David Loeffler might have already contributed similar lemmas a little while ago; I've tagged him in the PR too.