Theorems · Theorem · linear algebra
Matrix.spectrum_toLpLin
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
(p : ENNReal), spectrum 𝕜 ((Matrix.toLpLin p p) A) = spectrum 𝕜 AThe spectrum of a matrix A coincides with the spectrum of toLpLin p p A.
- Defined in
- Mathlib.Analysis.Matrix.Spectrum
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RCLikeFintypeDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- ENNRealstatement and proof · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- LinearEquivstatement · cited by 3,317
- RCLikestatement and proof · cited by 2,829
- spectrumstatement · cited by 510
- WithLpstatement · cited by 345
- Matrix.toLpLinstatement · cited by 14
Cited by2
Results whose statement or proof uses this declaration.
- Matrix.IsHermitian.eigenvalues_mem_spectrum_realproof · cited by 2
- Matrix.spectrum_toEuclideanLinproof · cited by 0