Theorems · Theorem · field theory

Module.Basis.norm_extends

∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L} {i : ι},
  B i = 1 → ∀ (x : K), B.norm ((algebraMap K L) x) = ‖x‖

For any K-basis B of L containing 1, B.norm extends the norm on K.

Defined in

Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldRingAlgebraFintypeNonempty