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 SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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.orthogonal	—	—

---

← Back to Index