Spectrum

📁 Source: Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Statistics

Metric	Count
Definitions diagonalization, directSumDecomposition, eigenvalues, eigenvectorBasis	4
Theorems eq_zero_of_forall_hasEigenvalue_eq_zero, finite_dimensional_eigenspace, orthogonalComplement_iSup_eigenspaces_eq_bot, apply_eigenvectorBasis, card_filter_eigenvalues_eq, charpoly_eq, conj_eigenvalue_eq_self, det_eq_prod_eigenvalues, diagonalization_apply_self_apply, diagonalization_symm_apply, directSum_decompose_apply, direct_sum_isInternal, eigenvalues_antitone, eigenvalues_def, eigenvalues_eq_eigenvalues_iff, eigenvectorBasis_apply_self_apply, eigenvectorBasis_def, exists_eigenvalues_eq, hasEigenvalue_eigenvalues, hasEigenvector_eigenvectorBasis, invariant_orthogonalComplement_eigenspace, orthogonalComplement_iSup_eigenspaces, orthogonalComplement_iSup_eigenspaces_eq_bot, orthogonalComplement_iSup_eigenspaces_eq_bot', orthogonalComplement_iSup_eigenspaces_invariant, orthogonalFamily_eigenspaces, orthogonalFamily_eigenspaces', roots_charpoly_eq_eigenvalues, sort_roots_charpoly_eq_eigenvalues, splits_charpoly, toMatrix_eigenvectorBasis, eigenvalue_nonneg_of_nonneg, eigenvalue_pos_of_pos, inner_product_apply_eigenvector	34
Total	38

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_forall_hasEigenvalue_eq_zero 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace funLike LinearMap.IsSymmetric toLinearMap	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace zero	—	RingHomIsometric.ids nnnorm_eq_zero ENNReal.coe_eq_zero SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul spectralRadius_eq_nnnorm LinearMap.IsSymmetric.isSelfAdjoint spectralRadius.eq_1 not_iff_not ENNReal.iSup_eq_zero Mathlib.Tactic.Push.not_forall_eq NeZero.charZero_one IsCompactOperator.hasEigenvalue_iff_mem_spectrum
finite_dimensional_eigenspace 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace funLike	FiniteDimensional Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Module.End.eigenspace toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Submodule.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.module	—	Module.End.mem_invtSubmodule_iff_forall_mem_of_mem Module.End.eigenspace_mem_invtSubmodule IsCompactOperator.restrict' T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe isClosed_eigenspace UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.left isCompactOperator_id_iff_finiteDimensional RCLike.toCompleteSpace locallyCompact_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real IsCompactOperator.smul_iff₀ ContinuousSMul.continuousConstSMul SMulMemClass.continuousSMul IsBoundedSMul.continuousSMul Submodule.smulMemClass smulCommClass_self LinearMap.coe_smul Module.End.restrict_eigenspace
orthogonalComplement_iSup_eigenspaces_eq_bot 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace funLike LinearMap.IsSymmetric toLinearMap	Submodule.orthogonal iSup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup toLinearMap RingHom.id Semiring.toNonAssocSemiring Bot.bot Submodule.instBot	—	LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant LinearMap.continuous_domRestrict continuous_toLinearMap IsCompactOperator.restrict' T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity Submodule.instOrthogonalCompleteSpace LinearMap.IsSymmetric.restrict_invariant Submodule.eq_bot_iff Submodule.coe_zero Submodule.mem_bot Submodule.inf_orthogonal_eq_bot Submodule.mem_iSup_of_mem Module.End.mem_eigenspace_iff NeZero.charZero_one instIsEmptyFalse Submodule.subsingleton_iff_eq_bot eq_zero_of_forall_hasEigenvalue_eq_zero Module.End.eigenspace_zero LinearMap.ker_zero Submodule.instNontrivial

LinearMap.IsSymmetric

Definitions

Name	Category	Theorems
diagonalization 📖	CompOp	2 math math: diagonalization_apply_self_apply, diagonalization_symm_apply
directSumDecomposition 📖	CompOp	1 math math: directSum_decompose_apply
eigenvalues 📖	CompOp	21 math math: LinearMap.IsPositive.nonneg_eigenvalues, card_filter_eigenvalues_eq, hasEigenvalue_eigenvalues, eigenvectorBasis_apply_self_apply, LinearMap.singularValues_fin, LinearMap.sq_singularValues_of_lt, LinearMap.sq_singularValues_fin, apply_eigenvectorBasis, eigenvalues_def, det_eq_prod_eigenvalues, trace_eq_sum_eigenvalues, roots_charpoly_eq_eigenvalues, charpoly_eq, exists_eigenvalues_eq, LinearMap.singularValues_of_lt, re_trace_eq_sum_eigenvalues, toMatrix_eigenvectorBasis, hasEigenvector_eigenvectorBasis, sort_roots_charpoly_eq_eigenvalues, eigenvalues_antitone, eigenvalues_eq_eigenvalues_iff
eigenvectorBasis 📖	CompOp	5 math math: eigenvectorBasis_apply_self_apply, apply_eigenvectorBasis, toMatrix_eigenvectorBasis, hasEigenvector_eigenvectorBasis, eigenvectorBasis_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eigenvectorBasis 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike OrthonormalBasis Fin.fintype OrthonormalBasis.instFunLike eigenvectorBasis SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RCLike.ofReal eigenvalues	—	Module.End.mem_eigenspace_iff hasEigenvector_eigenvectorBasis
card_filter_eigenvalues_eq 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Finset.card Finset.filter RCLike.ofReal eigenvalues RCLike.toDecidableEq Finset.univ Fin.fintype Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Module.End.eigenspace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module	—	eigenvalues_def Finset.card_equiv
charpoly_eq 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	LinearMap.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.Free.of_divisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RCLike.ofReal eigenvalues	—	Module.Free.of_divisionRing RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.charpoly_toMatrix Matrix.charpoly.congr_simp toMatrix_eigenvectorBasis Matrix.charpoly_diagonal Finset.prod_congr
conj_eigenvalue_eq_self 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike starRingEnd RCLike.toStarRing	—	Module.End.HasEigenvalue.exists_hasEigenvector Module.End.mem_eigenspace_iff inner_smul_left inner_self_eq_norm_sq_to_K inner_smul_right IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
det_eq_prod_eigenvalues 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det Finset.prod CommRing.toCommMonoid Finset.univ Fin.fintype RCLike.ofReal eigenvalues	—	instIsDomain Module.Free.of_divisionRing Module.End.det_eq_prod_roots_charpoly_of_splits splits_charpoly roots_charpoly_eq_eigenvalues Multiset.map_congr Fin.univ_val_map List.prod_ofFn
diagonalization_apply_self_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Module.End.instFintypeEigenvalues instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Submodule.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike diagonalization LinearMap LinearMap.instFunLike Submodule.smul Algebra.toSMul Semifield.toCommSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsScalarTower.left Module.End.mem_eigenspace_iff diagonalization_symm_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearIsometryEquiv.symm_apply_apply LinearIsometryEquiv.apply_symm_apply
diagonalization_symm_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Module.End.instFintypeEigenvalues instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module Submodule.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm diagonalization Finset.sum Finset.univ WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors direct_sum_isInternal orthogonalFamily_eigenspaces'
directSum_decompose_apply 📖	mathematical	—	DFunLike.coe DFinsupp Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat DFinsupp.instDFunLike Equiv DirectSum AddSubmonoidClass.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.addSubmonoidClass EquivLike.toFunLike Equiv.instEquivLike DirectSum.decompose Module.End.UnivEigenvalues.instDecidableEq RCLike.toDecidableEq directSumDecomposition ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Submodule.orthogonalProjection Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.finiteDimensional_submodule NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Submodule.addSubmonoidClass
direct_sum_isInternal 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	DirectSum.IsInternal Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.End.UnivEigenvalues.instDecidableEq RCLike.toDecidableEq ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.addSubmonoidClass Module.End.eigenspace Module.End.UnifEigenvalues.val	—	Submodule.addSubmonoidClass OrthogonalFamily.isInternal_iff orthogonalFamily_eigenspaces' orthogonalComplement_iSup_eigenspaces_eq_bot'
eigenvalues_antitone 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Antitone Real PartialOrder.toPreorder Fin.instPartialOrder Real.instPreorder eigenvalues	—	eigenvalues_def Function.comp_assoc Monotone.comp_antitone Tuple.monotone_sort
eigenvalues_def 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	eigenvalues Real DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Tuple.sort Real.linearOrder Fin.revPerm	—	—
eigenvalues_eq_eigenvalues_iff 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	eigenvalues LinearMap.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.Free.of_divisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Module.Free.of_divisionRing charpoly_eq instIsDomain instIsTransGe instAntisymmGe LE.total' sort_roots_charpoly_eq_eigenvalues
eigenvectorBasis_apply_self_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EuclideanSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Fin.fintype NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedSpace.toModule InnerProductSpace.toNormedSpace WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing RCLike.innerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike OrthonormalBasis.repr eigenvectorBasis LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing RCLike.ofReal eigenvalues	—	RingHomInvPair.ids fact_one_le_two_ennreal Nat.instAtLeastTwoHAddOfNat Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass apply_eigenvectorBasis Fintype.sum_congr smul_smul mul_comm WithLp.ofLp_toLp LinearIsometryEquiv.symm_apply_apply LinearIsometryEquiv.apply_symm_apply
eigenvectorBasis_def 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	eigenvectorBasis OrthonormalBasis.reindex Fin.fintype DirectSum.IsInternal.subordinateOrthonormalBasis Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.End.instFintypeEigenvalues Module.End.UnivEigenvalues.instDecidableEq RCLike.toDecidableEq ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat Module.End.eigenspace Module.End.UnifEigenvalues.val direct_sum_isInternal orthogonalFamily_eigenspaces' Equiv.symm Equiv.Perm Equiv.Perm.instMul Tuple.sort Real Real.linearOrder Fin.revPerm	—	direct_sum_isInternal orthogonalFamily_eigenspaces'
exists_eigenvalues_eq 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedAddCommGroup.toAddCommGroup	RCLike.ofReal eigenvalues	—	eigenvalues_def Equiv.apply_symm_apply
hasEigenvalue_eigenvalues 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace RCLike.ofReal eigenvalues	—	Module.End.hasEigenvalue_of_hasEigenvector hasEigenvector_eigenvectorBasis
hasEigenvector_eigenvectorBasis 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Module.End.HasEigenvector EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace RCLike.ofReal eigenvalues DFunLike.coe OrthonormalBasis Fin.fintype OrthonormalBasis.instFunLike eigenvectorBasis	—	eigenvalues_def direct_sum_isInternal orthogonalFamily_eigenspaces' eigenvectorBasis_def OrthonormalBasis.reindex_apply
invariant_orthogonalComplement_eigenspace 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Module.End.mem_eigenspace_iff inner_smul_left MulZeroClass.mul_zero
orthogonalComplement_iSup_eigenspaces 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Module.End.eigenspace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Field.toCommRing SeminormedAddCommGroup.toAddCommGroup EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup Submodule.module LinearMap.restrict orthogonalComplement_iSup_eigenspaces_invariant Bot.bot CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	Module.End.eigenspace_restrict_eq_bot orthogonalComplement_iSup_eigenspaces_invariant Submodule.IsOrtho.mono_left le_iSup Submodule.isOrtho_orthogonal_right Submodule.IsOrtho.disjoint
orthogonalComplement_iSup_eigenspaces_eq_bot 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.orthogonal iSup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup Bot.bot Submodule.instBot	—	orthogonalComplement_iSup_eigenspaces_invariant restrict_invariant Submodule.eq_bot_of_subsingleton subsingleton_of_no_eigenvalue_finiteDimensional FiniteDimensional.finiteDimensional_submodule orthogonalComplement_iSup_eigenspaces
orthogonalComplement_iSup_eigenspaces_eq_bot' 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.orthogonal iSup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedAddCommGroup.toAddCommGroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat Bot.bot Submodule.instBot	—	iSup_ne_bot_subtype orthogonalComplement_iSup_eigenspaces_eq_bot
orthogonalComplement_iSup_eigenspaces_invariant 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Submodule.iInf_orthogonal LinearMap.iInf_invariant invariant_orthogonalComplement_eigenspace
orthogonalFamily_eigenspaces 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Module.End.eigenspace Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ	—	inner_zero_left conj_eigenvalue_eq_self Module.End.hasEigenvalue_of_hasEigenvector Module.End.mem_eigenspace_iff inner_smul_right inner_smul_left IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
orthogonalFamily_eigenspaces' 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ	—	OrthogonalFamily.comp orthogonalFamily_eigenspaces Subtype.coe_injective
roots_charpoly_eq_eigenvalues 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField instIsDomain Field.toSemifield LinearMap.charpoly NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.Free.of_divisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Multiset.map Real RCLike.ofReal eigenvalues Finset.val Finset.univ Fin.fintype	—	instIsDomain Module.Free.of_divisionRing RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.charpoly_toMatrix toMatrix_eigenvectorBasis Matrix.charpoly_diagonal Polynomial.roots_prod Finset.prod_congr Polynomial.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.instNoZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Polynomial.roots_X_sub_C Multiset.bind_singleton Fin.univ_val_map Multiset.map_congr
sort_roots_charpoly_eq_eigenvalues 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Multiset.sort Real Multiset.map DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield LinearMap.charpoly NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.Free.of_divisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Real.instLE Real.decidableLE instIsTransGe Real.instPreorder instAntisymmGe Real.partialOrder LE.total' Real.linearOrder eigenvalues	—	instIsDomain Module.Free.of_divisionRing instIsTransGe instAntisymmGe LE.total' Multiset.sort.congr_simp Multiset.map_congr roots_charpoly_eq_eigenvalues Fin.univ_val_map RCLike.ofReal_re Antitone.sortedGE_ofFn eigenvalues_antitone
splits_charpoly 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField LinearMap.charpoly NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Module.Free.of_divisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Module.Free.of_divisionRing instIsDomain Polynomial.splits_iff_card_roots roots_charpoly_eq_eigenvalues Multiset.map_congr Fin.univ_val_map LinearMap.charpoly_natDegree IsLocalRing.toNontrivial Field.instIsLocalRing commRing_strongRankCondition
toMatrix_eigenvectorBasis 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Fin.fintype Finite.of_fintype OrthonormalBasis.toBasis eigenvectorBasis Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Real RCLike.ofReal eigenvalues	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_apply apply_eigenvectorBasis map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass algebraMap_smul Finsupp.isScalarTower IsScalarTower.right fact_one_le_two_ennreal OrthonormalBasis.coe_toBasis_repr_apply OrthonormalBasis.repr_self PiLp.single_apply smul_ite RCLike.real_smul_eq_coe_mul mul_one smul_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eigenvalue_nonneg_of_nonneg 📖	mathematical	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace RCLike.ofReal Real Real.instLE Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike	Real Real.instLE Real.instZero	—	Module.End.HasEigenvalue.exists_hasEigenvector Real.instIsStrictOrderedRing AddGroup.existsAddOfLE RCLike.ofReal_re inner_product_apply_eigenvector mul_nonneg_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono
eigenvalue_pos_of_pos 📖	mathematical	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace RCLike.ofReal Real Real.instLT Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike	Real Real.instLT Real.instZero	—	Module.End.HasEigenvalue.exists_hasEigenvector Real.instIsStrictOrderedRing AddGroup.existsAddOfLE RCLike.ofReal_re inner_product_apply_eigenvector mul_pos_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE
inner_product_apply_eigenvector 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm	—	inner_smul_right inner_self_eq_norm_sq_to_K

---

← Back to Index