OAI/Analysis/Pureness/States/RegularizedStateFreeGroupExactness.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.CuntzPureness.regularizedStateCauchyPositiveline 12 - abbrev
OAI.CuntzPureness.regularizedStateCauchyTriangleline 19 - lemma
OAI.CuntzPureness.regularizedStateCauchyPositive_quotientline 26 - theorem
OAI.CuntzPureness.regularizedStateFreeGroupTensor_kernelline 31