English
There exists a real-linear isometry between 𝕜 (with RCLike structure) and ℂ, compatible with the complex structure, extending the complex Ring Equiv.
Русский
Существует вещеально-линейное изометрическое отображение между 𝕜 (с структурой RCLike) и ℂ, совместимое с комплексной структурой, согласующееся с комплексным изоморфизмом.
LaTeX
$$$\\exists \\, \phi: 𝕜 \\to[\\mathbb{R}] \\mathbb{C} \\\\text{— isometry such that } \\phi(x) = \\Re x + i \\Im x$$$
Lean4
/-- The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when
`RCLike.im RCLike.I = 1`. -/
@[simps]
def _root_.RCLike.complexLinearIsometryEquiv {𝕜 : Type*} [RCLike 𝕜] (h : RCLike.im (RCLike.I : 𝕜) = 1) : 𝕜 ≃ₗᵢ[ℝ] ℂ
where
map_smul' _ _ := by simp [RCLike.smul_re, RCLike.smul_im, ofReal_mul]; ring
norm_map'
_ :=
by
rw [← sq_eq_sq₀ (by positivity) (by positivity), ← normSq_eq_norm_sq, ← RCLike.normSq_eq_def', RCLike.normSq_apply]
simp [normSq_add]
__ := RCLike.complexRingEquiv h
