Theorems · Theorem · field theory

Module.Basis.norm_isNonarchimedean

∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L}, IsNonarchimedean norm → IsNonarchimedean B.norm

For any K-basis of L, if the norm on K is nonarchimedean, then so is B.norm.

Defined in

Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedFieldRingAlgebraFintypeNonempty