Semisimple

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

Statistics

Metric	Count
Definitions	0
Theorems isFinitelySemisimple, orthogonalComplement_mem_invtSubmodule	2
Total	2

LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelySemisimple 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Module.End.IsFinitelySemisimple EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace	—	Module.End.isFinitelySemisimple_iff inf_le_right Module.End.invtSubmodule.inf_mem orthogonalComplement_mem_invtSubmodule Submodule.inf_orthogonal_eq_bot inf_of_le_left Submodule.finiteDimensional_of_le Submodule.sup_orthogonal_of_hasOrthogonalProjection Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule sup_inf_assoc_of_le Submodule.instIsModularLattice top_inf_eq
orthogonalComplement_mem_invtSubmodule 📖	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 Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	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 Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Submodule.orthogonal	—	—

---

← Back to Index