Documentation Verification Report

Basic

📁 Source: Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

Statistics

Metric	Count
Definitions `VonNeumannAlgebra`, `commutant`, `instPartialOrder`, `instSetLike`, `toStarSubalgebra`, `WStarAlgebra`	6
Theorems `mem_iff`, `mem_iff`, `centralizer_centralizer`, `centralizer_centralizer'`, `coe_commutant`, `coe_mk`, `coe_toStarSubalgebra`, `commutant_commutant`, `ext`, `ext_iff`, `instStarMemClass`, `instSubringClass`, `mem_carrier`, `mem_commutant_iff`, `exists_predual`	15
Total	21

VonNeumannAlgebra

Definitions

Name	Category	Theorems
`commutant` 📖	CompOp	3 math math: `commutant_commutant`, `mem_commutant_iff`, `coe_commutant`
`instPartialOrder` 📖	CompOp	—
`instSetLike` 📖	CompOp	11 math math: `ext_iff`, `coe_mk`, `mem_carrier`, `centralizer_centralizer`, `IsIdempotentElem.mem_iff`, `IsStarProjection.mem_iff`, `coe_toStarSubalgebra`, `mem_commutant_iff`, `coe_commutant`, `instStarMemClass`, `instSubringClass`
`toStarSubalgebra` 📖	CompOp	3 math math: `centralizer_centralizer'`, `mem_carrier`, `coe_toStarSubalgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centralizer_centralizer` 📖	mathematical	—	`Set.centralizer` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `SetLike.coe` `VonNeumannAlgebra` `instSetLike` `ContinuousLinearMap.instMul`	—	`centralizer_centralizer'`
`centralizer_centralizer'` 📖	mathematical	—	`Set.centralizer` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `ContinuousLinearMap.semiring` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subalgebra.toSubsemiring` `Complex.instCommSemiring` `ContinuousLinearMap.algebra` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `StarSubalgebra.toSubalgebra` `Complex.instStarRing` `ContinuousLinearMap.instStarRingId` `ContinuousLinearMap.instStarModuleId` `toStarSubalgebra` `ContinuousLinearMap.instMul`	—	—
`coe_commutant` 📖	mathematical	—	`SetLike.coe` `VonNeumannAlgebra` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `instSetLike` `commutant` `Set.centralizer` `ContinuousLinearMap.instMul`	—	`StarMemClass.star_coe_eq` `instStarMemClass` `Set.union_self`
`coe_mk` 📖	mathematical	`Set.centralizer` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `ContinuousLinearMap.semiring` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subalgebra.toSubsemiring` `Complex.instCommSemiring` `ContinuousLinearMap.algebra` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `StarSubalgebra.toSubalgebra` `Complex.instStarRing` `ContinuousLinearMap.instStarRingId` `ContinuousLinearMap.instStarModuleId` `ContinuousLinearMap.instMul`	`SetLike.coe` `VonNeumannAlgebra` `instSetLike` `StarSubalgebra` `StarSubalgebra.setLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId`
`coe_toStarSubalgebra` 📖	mathematical	—	`SetLike.coe` `StarSubalgebra` `Complex` `ContinuousLinearMap` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `Complex.instCommSemiring` `Complex.instStarRing` `ContinuousLinearMap.semiring` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instStarRingId` `ContinuousLinearMap.algebra` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId` `StarSubalgebra.setLike` `toStarSubalgebra` `VonNeumannAlgebra` `instSetLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId`
`commutant_commutant` 📖	mathematical	—	`commutant`	—	`SetLike.coe_injective` `coe_commutant` `centralizer_centralizer`
`ext` 📖	—	`ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `VonNeumannAlgebra` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `VonNeumannAlgebra` `SetLike.instMembership` `instSetLike`	—	`ext`
`instStarMemClass` 📖	mathematical	—	`StarMemClass` `VonNeumannAlgebra` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `ContinuousLinearMap.instStarId` `instSetLike`	—	`StarSubalgebra.star_mem'` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId`
`instSubringClass` 📖	mathematical	—	`SubringClass` `VonNeumannAlgebra` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `ContinuousLinearMap.ring` `Complex.instRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSetLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Subsemigroup.mul_mem'` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId` `Submonoid.one_mem'` `Subsemiring.add_mem'` `Subsemiring.zero_mem'` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `StarSubalgebra.subringClass`
`mem_carrier` 📖	mathematical	—	`ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `ContinuousLinearMap.semiring` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instStarRingId` `ContinuousLinearMap.algebra` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId` `SetLike.instMembership` `StarSubalgebra.setLike` `toStarSubalgebra` `Set` `Set.instMembership` `SetLike.coe` `VonNeumannAlgebra` `instSetLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarModuleId`
`mem_commutant_iff` 📖	mathematical	—	`ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `VonNeumannAlgebra` `SetLike.instMembership` `instSetLike` `commutant` `ContinuousLinearMap.instMul`	—	`SetLike.mem_coe` `coe_commutant`

VonNeumannAlgebra.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_iff` 📖	mathematical	`IsIdempotentElem` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `ContinuousLinearMap.instMul`	`VonNeumannAlgebra` `SetLike.instMembership` `VonNeumannAlgebra.instSetLike` `Submodule` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Sublattice.instSetLike` `Module.End.invtSubmodule` `ContinuousLinearMap.toLinearMap` `LinearMap.range` `RingHomSurjective.ids` `LinearMap.ker`	—	`RingHomSurjective.ids` `ContinuousLinearMap.IsIdempotentElem.commute_iff` `Commute.symm_iff` `VonNeumannAlgebra.commutant_commutant`

VonNeumannAlgebra.IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_iff` 📖	mathematical	`IsStarProjection` `ContinuousLinearMap` `Complex` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `ContinuousLinearMap.instMul` `ContinuousLinearMap.instStarId`	`VonNeumannAlgebra` `SetLike.instMembership` `VonNeumannAlgebra.instSetLike` `Submodule` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Sublattice.instSetLike` `Module.End.invtSubmodule` `ContinuousLinearMap.toLinearMap` `LinearMap.range` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `VonNeumannAlgebra.IsIdempotentElem.mem_iff` `IsStarProjection.isIdempotentElem` `RingHomCompTriple.ids` `ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff` `ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff` `StarMul.star_mul` `IsSelfAdjoint.star_eq` `IsStarProjection.isSelfAdjoint` `star_star` `StarMemClass.star_mem` `VonNeumannAlgebra.instStarMemClass`

WStarAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_predual` 📖	mathematical	—	`LinearIsometryEquiv` `Complex` `CommSemiring.toSemiring` `Complex.instCommSemiring` `starRingEnd` `Complex.instStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `Complex.instSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.instModuleSelf` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	—

(root)

Definitions

Name	Category	Theorems
`VonNeumannAlgebra` 📖	CompData	11 math math: `VonNeumannAlgebra.ext_iff`, `VonNeumannAlgebra.coe_mk`, `VonNeumannAlgebra.mem_carrier`, `VonNeumannAlgebra.centralizer_centralizer`, `VonNeumannAlgebra.IsIdempotentElem.mem_iff`, `VonNeumannAlgebra.IsStarProjection.mem_iff`, `VonNeumannAlgebra.coe_toStarSubalgebra`, `VonNeumannAlgebra.mem_commutant_iff`, `VonNeumannAlgebra.coe_commutant`, `VonNeumannAlgebra.instStarMemClass`, `VonNeumannAlgebra.instSubringClass`
`WStarAlgebra` 📖	CompData	—

---

← Back to Index