English
Let K be a normed field and L a normed division ring which is a normed K-algebra. Then L is ultrametric if and only if K is ultrametric.
Русский
Пусть K — нормированное поле, L — нормированное делимое кольцо, являющееся нормированной K-алгеброй. Тогда L ультраметрично тогда и только тогда, когда K ультраметрично.
LaTeX
$$$$IsUltrametricDist\\,L \\iff IsUltrametricDist\\,K.$$$$
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 and only if `K` is.
-/
theorem normedAlgebra_iff [NormedDivisionRing L] [NormedAlgebra K L] : IsUltrametricDist L ↔ IsUltrametricDist K :=
⟨fun _ => IsUltrametricDist.of_normedAlgebra' L, fun _ => IsUltrametricDist.of_normedAlgebra K⟩
