Theorems · Theorem · several complex variables

UpperHalfPlane.hasDerivAt_denom_zpow

∀ (g : GL (Fin 2) ℝ) (k : ℤ) (τ : UpperHalfPlane),
  HasDerivAt (fun z => UpperHalfPlane.denom g z ^ k) (↑k * ↑(↑g 1 0) * UpperHalfPlane.denom g ↑τ ^ (k - 1)) ↑τ

Derivative of z ↦ (denom g z) ^ k: $\frac{d}{dz}[(cz+d)^k] = k \cdot c \cdot (cz+d)^{k-1}$.

Defined in

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Cited by

2 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound