English
Let K be a normed field and L a seminormed ring which is a normed K-algebra, with ||1|| = 1 in L. If the norm on L is ultrametric (nonarchimedean), then the norm on K is ultrametric.
Русский
Пусть K — нормированное поле, L —seminormed кольцо, являющееся нормированной K-алгеброй, и ||1|| = 1 в L. Тогда норма на K является ультраметрической.
LaTeX
$$$$\\forall x,y,z \\in K:\\quad \\|x - z\\| \\le \\max\\{\\|x - y\\|, \\|y - z\\|\\}. $$$$
Lean4
/-- The other direction of `IsUltrametricDist.of_normedAlgebra`.
Let `K` be a normed field. If a seminormed ring `L` is a normed `K`-algebra, and `‖1‖ = 1` in `L`,
then `K` is ultrametric (i.e. the norm on `L` is nonarchimedean) if `F` is.
This can be further generalized to the case where `‖1‖ ≠ 0` in `L`.
-/
theorem of_normedAlgebra' [SeminormedRing L] [NormOneClass L] [NormedAlgebra K L] [h : IsUltrametricDist L] :
IsUltrametricDist K :=
⟨fun x y z => by simpa using h.dist_triangle_max (algebraMap K L x) (algebraMap K L y) (algebraMap K L z)⟩
