JointEigenspace

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

Statistics

Metric	Count
Definitions	0
Theorems directSum_isInternal_of_pairwise_commute, directSum_isInternal_of_commute, iSup_eigenspace_inf_eigenspace_of_commute, iSup_iInf_eq_top_of_commute, iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, orthogonalFamily_eigenspace_inf_eigenspace, orthogonalFamily_iInf_eigenspaces	7
Total	7

LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum_isInternal_of_commute 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Commute 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 Module.End.instMul	DirectSum.IsInternal Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RCLike.toDecidableEq Submodule.setLike Submodule.addSubmonoidClass Submodule.instMin Module.End.eigenspace	—	Submodule.addSubmonoidClass OrthogonalFamily.isInternal_iff orthogonalFamily_eigenspace_inf_eigenspace Submodule.orthogonal_eq_bot_iff Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.finiteDimensional_submodule iSup_prod iSup_comm iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute
iSup_eigenspace_inf_eigenspace_of_commute 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Commute 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 Module.End.instMul	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instMin Module.End.eigenspace	—	RingHomSurjective.ids Submodule.map_subtype_top Module.End.mapsTo_genEigenspace_of_comm Submodule.inf_genEigenspace Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule IsScalarTower.left FiniteDimensional.finiteDimensional_submodule orthogonalComplement_iSup_eigenspaces_eq_bot restrict_invariant
iSup_iInf_eq_top_of_commute 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Pairwise Function.onFun 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 Commute Module.End.instMul	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice iInf Submodule.instInfSet Module.End.eigenspace Top.top Submodule.instTop	—	Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace isFinitelySemisimple Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute Submodule.orthogonal_eq_bot_iff Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.finiteDimensional_submodule orthogonalComplement_iSup_eigenspaces_eq_bot
iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Commute 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 Module.End.instMul	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instMin Module.End.eigenspace Top.top Submodule.instTop	—	iSup_eigenspace_inf_eigenspace_of_commute Submodule.orthogonal_eq_bot_iff Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.finiteDimensional_submodule orthogonalComplement_iSup_eigenspaces_eq_bot
orthogonalFamily_eigenspace_inf_eigenspace 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily 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.instMin Module.End.eigenspace EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	OrthogonalFamily.of_pairwise not_and_or Ne.eq_def OrthogonalFamily.pairwise orthogonalFamily_eigenspaces
orthogonalFamily_iInf_eigenspaces 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily 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 iInf Submodule.instInfSet Module.End.eigenspace EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Function.ne_iff orthogonalFamily_eigenspaces Submodule.mem_iInf

LinearMap.IsSymmetric.LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum_isInternal_of_pairwise_commute 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Pairwise Function.onFun Module.End 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 Commute Module.End.instMul	DirectSum.IsInternal Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Submodule.setLike Submodule.addSubmonoidClass iInf Submodule.instInfSet Module.End.eigenspace	—	Submodule.addSubmonoidClass OrthogonalFamily.isInternal_iff LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute Submodule.top_orthogonal_eq_bot

---

← Back to Index