English
A complex-valued function is conformal at z if it is holomorphic at z with a nonzero derivative.
Русский
Отображение комплексного значения конформно в точке z, если оно-Holomorphic в z и его производная не равна нулю.
LaTeX
$$$\text{DifferentiableAt}_{\mathbb{C}} f z \land \operatorname{deriv} f z \neq 0 \Rightarrow \text{ConformalAt} f z$$$
Lean4
/-- A real differentiable function of the complex plane into some complex normed space `E` is
conformal at a point `z` if it is holomorphic at that point with a nonvanishing differential.
This is a version of the Cauchy-Riemann equations. -/
theorem conformalAt (h : DifferentiableAt ℂ f z) (hf' : deriv f z ≠ 0) : ConformalAt f z :=
by
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
apply isConformalMap_complex_linear
simpa only [Ne, ContinuousLinearMap.ext_ring_iff]
