Theorems · Definition · field theory

IsUltrametricDist.invariantExtension

(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] → AlgebraNorm K L

The function L → ℝ sending x : L to the maximum of algNormOfAlgEquiv hna σ over all σ : L ≃ₐ[K] L is an algebra norm on L.

Defined in

Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedFieldFieldAlgebraFiniteDimensionalIsUltrametricDist