English
If map : ℂ →L[ℂ] E is a nonzero complex‑linear map, then its restriction to real scalars is conformal.
Русский
Если карта map : ℂ →L[ℂ] E не равна нулю и является комплексно-линейной, то её ограничение к действительным скалярам конформно.
LaTeX
$$$ map \neq 0 \Rightarrow IsConformalMap (map.restrictScalars \mathbb{R})$$$
Lean4
theorem isConformalMap_complex_linear {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : IsConformalMap (map.restrictScalars ℝ) :=
by
have minor₁ : ‖map 1‖ ≠ 0 := by simpa only [ContinuousLinearMap.ext_ring_iff, Ne, norm_eq_zero] using nonzero
refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
· intro x
simp only [LinearMap.smul_apply]
have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
nth_rw 1 [this]
rw [LinearMap.coe_restrictScalars]
simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
field_simp
· ext1
simp [minor₁]
