deriv_circleMap — Mathlib

English

For all c ∈ ℂ, R ∈ ℝ and θ ∈ ℝ, the derivative of circleMap at θ is circleMap(0,R,θ) · i.

Русский

Во всех c ∈ ℂ, R ∈ ℝ и θ ∈ ℝ производная circleMap(c,R,θ) равна circleMap(0,R,θ) · i.

LaTeX

$$$\forall c\in\mathbb{C},\; R\in\mathbb{R},\; \theta\in\mathbb{R},\; \frac{d}{d\theta} circleMap(c,R,\theta) = i\, circleMap(0,R,\theta).$$$

Lean4

@[simp]
theorem deriv_circleMap (c : ℂ) (R : ℝ) (θ : ℝ) : deriv (circleMap c R) θ = circleMap 0 R θ * I :=
  (hasDerivAt_circleMap _ _ _).deriv

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