Documentation
LeanPool
.
ConnesRigidity
.
Imports
Search
return to top
source
Imports
Init
LeanPool.ConnesRigidity
LeanPool.ConnesRigidity.Construction
LeanPool.ConnesRigidity.Core
LeanPool.ConnesRigidity.Main
LeanPool.ConnesRigidity.Construction.PaperActionInstances
LeanPool.ConnesRigidity.Construction.PaperActions
LeanPool.ConnesRigidity.Construction.SquareSpan
LeanPool.ConnesRigidity.Paper.Section3
LeanPool.ConnesRigidity.Paper.Section4
LeanPool.ConnesRigidity.Paper.Section5
LeanPool.ConnesRigidity.Paper.Section6
LeanPool.ConnesRigidity.Paper.Section7
LeanPool.ConnesRigidity.Porting.CoreTransfer
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4Basic
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificate
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard0
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard1
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard2
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard3
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard4
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard5
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard6
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelCertificateShard7
LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4KernelDetector
LeanPool.ConnesRigidity.Foundation.GroupTheory.SplitAbelianExtension
LeanPool.ConnesRigidity.Foundation.LinearAlgebra.ArithmeticSymplectic
LeanPool.ConnesRigidity.Foundation.LinearAlgebra.BooleanPolynomial
LeanPool.ConnesRigidity.Foundation.LinearAlgebra.QuadraticCocycle
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.BinaryPontryaginDual
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.CrossedProduct
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.CrossedProductFactorTransport
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.CrossedProductTransport
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.FactorWitness
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.FiniteIndex
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.FinitePropertyT
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.NormalFixed
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.NormalizedHaar
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.PositiveSpectralMeasure
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.PropertyTTransfer
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.SemidirectClosure
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.SemidirectFubini
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.SemidirectGeneratorTransport
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.SpectralCriterion
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.SpectralDetection
LeanPool.ConnesRigidity.Paper.Section3.CrossedAction
LeanPool.ConnesRigidity.Paper.Section3.CrossedHaar
LeanPool.ConnesRigidity.Paper.Section3.CrossedKernel
LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacy
LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacyAlgebra
LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacyCoordinates
LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacyFirst
LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacyQuadratic
LeanPool.ConnesRigidity.Paper.Section3.DualActions
LeanPool.ConnesRigidity.Paper.Section3.DualAutomorphism
LeanPool.ConnesRigidity.Paper.Section3.DualCoordinates
LeanPool.ConnesRigidity.Paper.Section3.DualHaar
LeanPool.ConnesRigidity.Paper.Section3.DualShearMeasure
LeanPool.ConnesRigidity.Paper.Section3.DualTopology
LeanPool.ConnesRigidity.Paper.Section3.FactorClosure
LeanPool.ConnesRigidity.Paper.Section3.FactorIsomorphism
LeanPool.ConnesRigidity.Paper.Section3.Fourier
LeanPool.ConnesRigidity.Paper.Section3.FourierAction
LeanPool.ConnesRigidity.Paper.Section3.FourierCoordinates
LeanPool.ConnesRigidity.Paper.Section3.GroupFactor
LeanPool.ConnesRigidity.Paper.Section3.GroupQuotient
LeanPool.ConnesRigidity.Paper.Section3.GroupVacuum
LeanPool.ConnesRigidity.Paper.Section3.QuotientAction
LeanPool.ConnesRigidity.Paper.Section4.AChartDetectorMeasure
LeanPool.ConnesRigidity.Paper.Section4.ChartDetector
LeanPool.ConnesRigidity.Paper.Section4.ChartDetectorMeasure
LeanPool.ConnesRigidity.Paper.Section4.ChartMeasure
LeanPool.ConnesRigidity.Paper.Section4.ChartOrbits
LeanPool.ConnesRigidity.Paper.Section4.ChartSpan
LeanPool.ConnesRigidity.Paper.Section4.FiniteCharts
LeanPool.ConnesRigidity.Paper.Section4.FiniteExtensions
LeanPool.ConnesRigidity.Paper.Section4.FullDetectorMeasure
LeanPool.ConnesRigidity.Paper.Section4.PropertyT
LeanPool.ConnesRigidity.Paper.Section4.SpectralDetector
LeanPool.ConnesRigidity.Paper.Section4.SpectralDetectorBridge
LeanPool.ConnesRigidity.Paper.Section4.SpectralFiniteDetection
LeanPool.ConnesRigidity.Paper.Section4.SpectralPropertyT
LeanPool.ConnesRigidity.Paper.Section4.SplitExtensions
LeanPool.ConnesRigidity.Paper.Section5.ICC
LeanPool.ConnesRigidity.Paper.Section5.ICCOrbits
LeanPool.ConnesRigidity.Paper.Section6.Characteristic
LeanPool.ConnesRigidity.Paper.Section6.CharacteristicTransport
LeanPool.ConnesRigidity.Paper.Section6.ModuleSemisimple
LeanPool.ConnesRigidity.Paper.Section6.ModuleSemisimpleTransport
LeanPool.ConnesRigidity.Paper.Section6.Nonisomorphism
LeanPool.ConnesRigidity.Paper.Section6.NonisomorphismEmbedding
LeanPool.ConnesRigidity.Paper.Section6.NonisomorphismProofs
LeanPool.ConnesRigidity.Paper.Section6.NonisomorphismTransport
LeanPool.ConnesRigidity.Paper.Section6.QuotientModuleTransport
LeanPool.ConnesRigidity.Paper.Section7.TheoremACompletion
LeanPool.ConnesRigidity.Foundation.GroupTheory.SpecialLinear.Basic
LeanPool.ConnesRigidity.Foundation.GroupTheory.SpecialLinear.ElementaryGeneration
LeanPool.ConnesRigidity.Foundation.GroupTheory.SpecialLinear.ICC
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.Projection.Supremum
LeanPool.ConnesRigidity.Foundation.OperatorAlgebra.Projection.ValuedSpectralMeasure
Imported by