Theorems · Theorem · functional analysis

IsUltrametricDist.normedAlgebra_iff

∀ (K : Type u_1) (L : Type u_2) [inst : NormedField K] [inst_1 : 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.

Defined in

Mathlib.Analysis.Normed.Algebra.Ultra

Cited by

0 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldNormedDivisionRingNormedAlgebra