Mathlib Map

Theorems · Theorem · commutative algebra

spectralNorm_zero

∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L], spectralNorm K L 0 = 0

spectralNorm K L (0 : L) = 0.

Defined in
Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Cited by
1 results in Mathlib
Foundations
Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldFieldAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

spectralAlgNorm · cited by 9spectralAlgNormspectralNorm_unique · cited by 3spectralNorm_uniqueReal · cited by 25697RealAlgebra · cited by 11388AlgebraField · cited by 7404FieldPolynomial · cited by 5681PolynomialPolynomial.X · cited by 1639Polynomial.XNormedField · cited by 1084NormedFieldpow_one · cited by 894pow_onespectralNorm · cited by 31spectralNormspectralValue · cited by 13spectralValuespectralValue_X_pow · cited by 2spectralValue_X_powminpoly.zero · cited by 2minpoly.zerospectralNorm_zeroCITED BYCITES

Cites11

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

Cited by2

Results whose statement or proof uses this declaration.