OAI/Analysis/Commutator/FreeNormalizer.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.FreeBlocks.innerRepresentation_conj_generatorline 34 - lemma
OAI.Kadison.FreeBlocks.innerRepresentation_conj_mem_generatedline 47 - lemma
OAI.Kadison.FreeBlocks.innerRepresentation_conj_mem_bicommutantline 61 - lemma
OAI.Kadison.FreeBlocks.innerRepresentation_vacuumline 71