differentiable_const_cpow_of_neZero

English

Let z ∈ ℂ with z ≠ 0. The map s ↦ z^{s} is differentiable on ℂ as a function of the complex variable s.

Русский

Пусть z ∈ ℂ и z ≠ 0. Функция s ↦ z^{s} дифференцируема по переменной s на ℂ.

LaTeX

$$$\\text{Let }z\\in\\mathbb{C},\\ z\\neq 0.\\quad s\\mapsto z^{s}\\text{ is differentiable on }\\mathbb{C}.$$$

Lean4

@[fun_prop]
theorem differentiable_const_cpow_of_neZero (z : ℂ) [NeZero z] : Differentiable ℂ fun s : ℂ ↦ z ^ s :=
  differentiable_id.const_cpow (.inl <| NeZero.ne z)

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