deriv_circleMap_eq_zero_iff — Mathlib

English

For any c ∈ ℂ, R ∈ ℝ and θ ∈ ℝ, deriv(circleMap c R)(θ) = 0 holds if and only if R = 0.

Русский

Для любых c ∈ ℂ, R ∈ ℝ и θ ∈ ℝ, deriv(circleMap(c,R))(θ) = 0 тогда и только тогда, когда R = 0.

LaTeX

$$$\frac{d}{d\theta} circleMap(c,R,\theta) = 0 \;\Longleftrightarrow\; R = 0.$$$

Lean4

theorem deriv_circleMap_eq_zero_iff {c : ℂ} {R : ℝ} {θ : ℝ} : deriv (circleMap c R) θ = 0 ↔ R = 0 := by simp [I_ne_zero]

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