Mathlib Map

Theorems · Definition · commutative algebra

spectralAlgNorm

(K : Type u_2) →
  [inst : NormedField K] →
    (L : Type u_3) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → [IsUltrametricDist K] → [h_alg : Algebra.IsAlgebraic K L] → AlgebraNorm K L

The spectral norm is a K-algebra norm on L.

Defined in
Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Cited by
9 results in Mathlib
Foundations
Depth 225 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldFieldAlgebraIsUltrametricDistAlgebra.IsAlgebraic
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

spectralMulAlgNorm · cited by 5spectralMulAlgNormspectralNorm_unique · cited by 3spectralNorm_uniquespectralAlgNorm_def · cited by 2spectralAlgNorm_defalgNormFromConst · cited by 2algNormFromConstNormedAlgebra.norm_eq_spectralNorm · cited by 1NormedAlgebra.norm_eq_spe…spectralAlgNorm_isPowMul · cited by 1spectralAlgNorm_isPowMulspectralAlgNorm_one · cited by 1spectralAlgNorm_onespectralAlgNorm_extends · cited by 0spectralAlgNorm_extendsspectralAlgNorm_mul · cited by 0spectralAlgNorm_mulspectralAlgNorm.congr_simp · cited by 0spectralAlgNorm.congr_simpalgNormFromConst_def · cited by 0algNormFromConst_defAlgebra · cited by 11388AlgebraField · cited by 7404FieldNormedField · cited by 1084NormedFieldAlgebra.IsAlgebraic · cited by 322Algebra.IsAlgebraicIsUltrametricDist · cited by 177IsUltrametricDistAlgebraNorm · cited by 39AlgebraNormspectralNorm · cited by 31spectralNormspectralNorm_zero · cited by 1spectralNorm_zerospectralAlgNormCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by11

Results whose statement or proof uses this declaration.