Theorems · Definition · commutative algebra
spectralNorm
(K : Type u_2) → [inst : NormedField K] → (L : Type u_3) → [inst_1 : Field L] → [Algebra K L] → L → ℝ
If L is an algebraic extension of a normed field K and y : L then the spectral norm
spectralNorm K y : ℝ of y (written |y|_sp in the textbooks) is the spectral value of the
minimal polynomial of y over K.
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedFieldFieldAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- NormedFieldstatement and proof · cited by 1,084
- minpolyproof · cited by 439
- spectralValueproof · cited by 13
Cited by33
Results whose statement or proof uses this declaration.
- spectralAlgNormproof · cited by 9
- spectralNorm.eq_of_normalClosurestatement · cited by 5
- spectralAlgNorm_of_finiteDimensional_normalproof · cited by 4
- spectralNorm_uniqueproof · cited by 3
- spectralNorm_zero_ltstatement · cited by 3
- isPowMul_spectralNormstatement and proof · cited by 3
- spectralAlgNorm_of_finiteDimensional_normal_defstatement · cited by 3
- spectralNorm_eq_invariantExtensionstatement · cited by 3
- spectralNorm_extendsstatement · cited by 3
- spectralAlgNorm_defstatement · cited by 2
- spectralNorm_eq_iSup_of_finiteDimensional_normalstatement · cited by 2
- spectralNorm_nonnegstatement · cited by 2