Normed algebra preserves ultrametricity

This file contains the proof that a normed division ring over an ultrametric field is ultrametric.

theorem IsUltrametricDist.of_normedAlgebra' {K : Type u_1} (L : Type u_2) [NormedField K] [SeminormedRing L] [NormOneClass L] [NormedAlgebra K L] [h : IsUltrametricDist L] : IsUltrametricDist K

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 IsUltrametricDist.of_normedAlgebra (K : Type u_1) {L : Type u_2} [NormedField K] [NormedDivisionRing L] [NormedAlgebra K L] [h : IsUltrametricDist K] : IsUltrametricDist L

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 IsUltrametricDist.normedAlgebra_iff (K : Type u_1) (L : Type u_2) [NormedField K] [NormedDivisionRing L] [NormedAlgebra K L] : IsUltrametricDist L ↔ IsUltrametricDist K

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.