OAI/Analysis/Commutator/ProperIsometryReplicas.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.Kadison.PartialIsometryOrder.Replicasline 18 - theorem
OAI.Kadison.PartialIsometryOrder.nonfinite_replicasline 25