algebraMap_isometry — Mathlib

English

In a normed algebra, the inclusion of the base field into the extended field is an isometry.

Русский

В нормированной алгебре вложение базового поля в расширенное поле является изометрией.

LaTeX

$$$\\operatorname{Isometry}(\\mathrm{algebraMap}_{\\mathbb{K} \\to \\mathbb{K}'})$$$

Lean4

/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
theorem algebraMap_isometry [NormOneClass 𝕜'] : Isometry (algebraMap 𝕜 𝕜') :=
  by
  refine Isometry.of_dist_eq fun x y => ?_
  rw [dist_eq_norm, dist_eq_norm, ← RingHom.map_sub, norm_algebraMap']

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