English
The distance between algebraMap x and algebraMap y equals distance x y multiplied by ∥1∥ in 𝕜'.
Русский
Расстояние между algebraMap(x) и algebraMap(y) равно расстоянию x,y, умноженному на ∥1∥ в 𝕜'.
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
/-- Any normed characteristic-zero division ring that is a normed algebra over the reals is also a
normed algebra over the rationals.
Phrased another way, if `𝕜` is a normed algebra over the reals, then `AlgebraRat` respects that
norm. -/
instance normedAlgebraRat {𝕜} [NormedDivisionRing 𝕜] [CharZero 𝕜] [NormedAlgebra ℝ 𝕜] : NormedAlgebra ℚ 𝕜 where
norm_smul_le q x := by rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_cast, norm_smul, Rat.norm_cast_real]
