English
Let K be a normed field. If a normed division ring L is a normed K-algebra, and K is ultrametric, then L is ultrametric.
Русский
Пусть K — нормированное поле. Если нормированное делимое кольцо L является нормированной K-алгеброй и K ультраметрично, то и L ультраметрично.
LaTeX
$$$$\\forall x,y,z \\in L:\\quad \\|x - z\\| \\le \\max\\{\\|x - y\\|, \\|y - z\\|\\}. $$$$
Lean4
/-- Let `K` be a normed field. If a normed division ring `L` is a normed `K`-algebra,
then `L` is ultrametric (i.e. the norm on `L` is nonarchimedean) if `K` is.
-/
theorem of_normedAlgebra [NormedDivisionRing L] [NormedAlgebra K L] [h : IsUltrametricDist K] : IsUltrametricDist L :=
by
rw [isUltrametricDist_iff_forall_norm_natCast_le_one] at h ⊢
exact fun n => (algebraMap.coe_natCast (R := K) (A := L) n) ▸ norm_algebraMap' L (n : K) ▸ h n
