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']