Theorems · Theorem · operator theory
LinearMap.IsSymmetric.hasEigenvalue_eigenvalues
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
(i : Fin n), Module.End.HasEigenvalue T ↑(hT.eigenvalues hn i)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement and proof · cited by 18,349
- NormedAddCommGroupstatement and proof · cited by 15,752
- LinearMapstatement and proof · cited by 10,215
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankstatement and proof · cited by 1,770
- RCLike.ofRealstatement · cited by 350
- LinearMap.IsSymmetricstatement and proof · cited by 121
- Module.End.HasEigenvaluestatement · cited by 56
- LinearMap.IsSymmetric.eigenvaluesstatement · cited by 31
- Module.End.hasEigenvalue_of_hasEigenvectorproof · cited by 8
Cited by3
Results whose statement or proof uses this declaration.
- Matrix.IsHermitian.eigenvalues_mem_spectrum_realproof · cited by 2
- LinearMap.injective_iff_forall_lt_finrank_singularValues_posproof · cited by 0
- LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValuesproof · cited by 0