realLinearIsometryEquiv — Mathlib

English

There is a real-linear isometry between K and ℝ when I = 0, given by a real ring isomorphism.

Русский

Существует линейно-изометрическое отображение между K и ℝ при I = 0, задающееся вещественным кольцевым изоморфизмом.

LaTeX

$$$$ realLinearIsometryEquiv (h : I = 0) : K \\simeq_{\\text{ℝ}}^{\\text{linear}} \\mathbb{R}. $$$$

Lean4

/-- The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when
`RCLike.I = 0`. -/
@[simps]
noncomputable def realLinearIsometryEquiv (h : I = (0 : K)) : K ≃ₗᵢ[ℝ] ℝ
    where
  map_smul' := smul_re
  norm_map' z := by rw [← re_add_im z]; simp [-re_add_im, h]
  __ := realRingEquiv h

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