star_conj — Mathlib

English

If HasDerivAt f f' x, then conj ∘ f ∘ conj has derivative conj f' at conj x.

Русский

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

LaTeX

$$theorem conj_conj {f : 𝕜 → F} {f' : F} (hf : HasDerivAt f f' x) : HasDerivAt (star ∘ f ∘ conj) (star f') (conj x)$$

Lean4

/-- If `f` has derivative `f'` at `z`, then `star ∘ f ∘ conj` has derivative `conj f'` at
`conj z`. -/
theorem star_conj {f : 𝕜 → F} {f' : F} (hf : HasDerivAt f f' x) : HasDerivAt (star ∘ f ∘ conj) (star f') (conj x) :=
  by
  rw [hasDerivAt_iff_hasFDerivAt]
  convert hf.hasFDerivAt.star_star
  ext
  simp

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