OAI/Analysis/BoundedHochschild/FactorFinitePaths.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Simultaneous fresh-path tests in diffuse finite factors.
- theorem
OAI.HochschildUltrapower.finitePathTests_of_factorline 42