Theorems · Theorem · functional analysis

IsUltrametricDist.of_normedAlgebra

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

Defined in

Mathlib.Analysis.Normed.Algebra.Ultra

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedDivisionRingNormedAlgebraIsUltrametricDist