conj_conj — Mathlib

English

If HasDerivAt f f' x, then conj ∘ f ∘ conj has derivative conj f' at conj x (equiv to HasDerivAt conj_conj).

Русский

Если есть HasDerivAt f f' x, то conj ∘ f ∘ conj имеет производную conj f' в conj x.

LaTeX

$$theorem conj_conj {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) : HasDerivAt (Function.comp (starRingEnd 𝕜) (Function.comp f (starRingEnd 𝕜))) (star f') (star x)$$

Lean4

/-- If `f` has derivative `f'` at `z`, then `conj ∘ f ∘ conj` has derivative `conj f'` at
`conj z`. -/
theorem conj_conj {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) : HasDerivAt (conj ∘ f ∘ conj) (conj f') (conj x) :=
  hf.star_conj

Похожие утверждения