Theorems · Theorem · field theory

IsUltrametricDist.invariantExtension_apply

∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (x : L),
  (IsUltrametricDist.invariantExtension K L) x = ⨆ σ, (IsUltrametricDist.algNormOfAlgEquiv σ) x

Defined in

Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedFieldFieldAlgebraFiniteDimensionalIsUltrametricDist