norm_algebraMap' — Mathlib

English

The distance between algebraMap(x) and algebraMap(y) equals distance(x,y) multiplied by the norm of 1 in 𝕜'.

Русский

Расстояние между algebraMap(x) и algebraMap(y) равно расстоянию(x,y) умноженному на норму единицы в 𝕜'.

LaTeX

$$$\\operatorname{dist}(\\mathrm{algebraMap}_{\\mathbb{K} \\to \\mathbb{K}'}(x), \\mathrm{algebraMap}_{\\mathbb{K} \\to \\mathbb{K}'}(y)) = \\operatorname{dist}(x,y) \\cdot \\|1_{\\mathbb{K}'}\\|$$$

Lean4

/-- This is a simpler version of `norm_algebraMap` when `‖1‖ = 1` in `𝕜'`. -/
@[simp]
theorem norm_algebraMap' [NormOneClass 𝕜'] (x : 𝕜) : ‖algebraMap 𝕜 𝕜' x‖ = ‖x‖ := by
  rw [norm_algebraMap, norm_one, mul_one]

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