OAI/Analysis/BoundedHochschild/ProperlyInfinitePrimitives.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_primitiveline 14 - theorem
OAI.BoundedHochschild.KadisonRingrose.properlyInfiniteVanishingInputline 35 - theorem
OAI.BoundedHochschild.KadisonRingrose.classicalVanishingInputline 44