isConformalMap_complex_linear_conj

English

If map ≠ 0, then (map restricted to ℝ) composed with conjugation is conformal.

Русский

Если map ≠ 0, то (map, ограниченная до ℝ) композиция с сопряжением конформна.

LaTeX

$$$ IsConformalMap ((map.restrictScalars \mathbb{R}).comp conjCLE.toContinuousLinearMap) $$

Lean4

theorem isConformalMap_complex_linear_conj {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
    IsConformalMap ((map.restrictScalars ℝ).comp (conjCLE : ℂ →L[ℝ] ℂ)) :=
  (isConformalMap_complex_linear nonzero).comp isConformalMap_conj

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