English
IsConformalMap g holds if and only if g is (up to restriction) complex-linear or conjugate-linear and g ≠ 0.
Русский
IsConformalMap g тогда и только тогда, когда g является (после ограничения) комплексно-линейной или сопряженно-линейной и g ≠ 0.
LaTeX
$$IsConformalMap g \iff ((\exists map, map.restrictScalars ℝ = g) ∨ (\exists map, map.restrictScalars ℝ = g ∘ conjCLE)) ∧ g ≠ 0$$
Lean4
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
-/
protected theorem complexOfReal {f' : ℂ →L[ℝ] E} (h₁ : HasFDerivWithinAt f f' s x) (h₂ : f' I = I • f' 1) :
HasFDerivWithinAt f (f'.complexOfReal h₂) s x :=
.of_restrictScalars ℝ h₁ rfl
