PaperFormalizer · Formalized papers
Formalized papers
Close Separable C^*-Algebras Without Spatial Conjugacy
Lean code
A standalone Lake project: the paper's Lean, the toolkit modules it imports, and
Check.lean
.
Check.lean
Papers/OaiCloseSeparableCstar/Basic.lean
Papers/OaiCloseSeparableCstar/Helpers/Ambient.lean
Papers/OaiCloseSeparableCstar/Helpers/AmbientCenter.lean
Papers/OaiCloseSeparableCstar/Helpers/AmbientCommutant.lean
Papers/OaiCloseSeparableCstar/Helpers/BadInclusion.lean
Papers/OaiCloseSeparableCstar/Helpers/FreeNorm.lean
Papers/OaiCloseSeparableCstar/Helpers/GoodInclusion.lean
Papers/OaiCloseSeparableCstar/Helpers/Invariant.lean
Papers/OaiCloseSeparableCstar/Helpers/LpOperators.lean
Papers/OaiCloseSeparableCstar/Helpers/OperatorMaps.lean
Papers/OaiCloseSeparableCstar/Helpers/SequenceAlgebra.lean
Papers/OaiCloseSeparableCstar/Helpers/SequenceConjugacy.lean
Papers/OaiCloseSeparableCstar/Helpers/TensorLp.lean
Papers/OaiCloseSeparableCstar/Helpers/Tree.lean
Papers/OaiCloseSeparableCstar/Helpers/TreeGram.lean
Papers/OaiCloseSeparableCstar/Helpers/TreeNorm.lean
Papers/OaiCloseSeparableCstar/Helpers/TreePathDiagonal.lean
Papers/OaiCloseSeparableCstar/Helpers/TreePathOperators.lean
Papers/OaiCloseSeparableCstar/Helpers/TreePerturbation.lean
Papers/OaiCloseSeparableCstar/Helpers/TreeUnitary.lean
Papers/OaiCloseSeparableCstar/Helpers/TreeVectors.lean
Papers/OaiCloseSeparableCstar/Helpers.lean
Papers/OaiCloseSeparableCstar/TMain.lean
Papers/OaiCloseSeparableCstar/TObstruction.lean
Papers/OaiCloseSeparableCstar/TSequences.lean
Papers/OaiCloseSeparableCstar.lean
Papers.lean
README.md
lakefile.toml
lean-toolchain