Theorems · Definition · field theory

Module.Basis.norm

{K : Type u_1} →
  {L : Type u_2} →
    [inst : NormedField K] →
      [inst_1 : Ring L] →
        [inst_2 : Algebra K L] → {ι : Type u_3} → [Fintype ι] → [Nonempty ι] → Module.Basis ι K L → L → ℝ

The function sending an element x : L to the maximum of the norms of its coefficients with respect to the K-basis B of L.

Defined in

Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Cited by

10 results in Mathlib

Foundations

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

Assumes

NormedFieldRingAlgebraFintypeNonempty