Theorems · Theorem · field theory

IsKrasner.of_completeSpace_of_normal

∀ (K : Type u_1) (L : Type u_2) [inst : NormedField L] [inst_1 : NontriviallyNormedField K] [CompleteSpace K]
  [IsUltrametricDist K] [inst_4 : NormedAlgebra K L] [Normal K L], IsKrasner K L

Krasner's lemma assuming Normal K L.

Defined in

Mathlib.Analysis.Normed.Field.Krasner

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldNontriviallyNormedFieldCompleteSpaceIsUltrametricDistNormedAlgebraNormal