English
If f has derivative f' at x and σ, σ' are inverse normed-ring automorphisms with σ isometric, then σ ∘ f ∘ σ' has derivative σ f' at σ x.
Русский
Если у f производная f' в x, и σ, σ' — обратные нормированные автоморфизмы колец с изометрией, то σ ∘ f ∘ σ' имеет производную σ f' в σ x.
LaTeX
$$$\text{If } f \text{ has derivative } f' \text{ at } x \text{ and } σ, σ' \text{ are inverse normed-ring automorphisms with } σ\text{ isometric}, \text{ then } σ \circ f \circ σ' \text{ has derivative } σ f' \text{ at } σ x.$$$
Lean4
/-- If `f` has derivative `f'` at `x`, and `σ, σ'` are mutually inverse normed-ring automorphisms,
then `σ ∘ f ∘ σ'` has derivative `σ f'` at `σ x`. -/
theorem comp_ringHom (hf : HasDerivAt f f' x) : HasDerivAt (σ ∘ f ∘ σ') (σ f') (σ x) :=
hf.comp_semilinear σ' ⟨σ.toSemilinearMap, σ.isometry.continuous⟩
