OAI/Analysis/Commutator/FreeSymmetry13.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Kadison.FreeBlocks.factorFullline 38 - abbrev
OAI.Kadison.FreeBlocks.factorZeroline 40 - def
OAI.Kadison.FreeBlocks.scalarGNSIsoline 44 - lemma
OAI.Kadison.FreeBlocks.letterGNSIso_preline 51