Theorems · Definition · field theory

IsUltrametricDist.algNormOfAlgEquiv

{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] → Gal(L/K) → AlgebraNorm K L

Given a normed field K, a finite algebraic extension L/K and σ : L ≃ₐ[K] L, the function L → ℝ sending x : L to ‖ σ x ‖, where ‖ ⬝ ‖ is any power-multiplicative algebra norm on L extending the norm on K, is an algebra norm on K.

Defined in

Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedFieldFieldAlgebraFiniteDimensionalIsUltrametricDist