OAI/Analysis/KadisonKastler/CommonRankFactorFibers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Factor fibers for a source and its commuting generating source

  1. theorem OAI.KadisonKastler.commonRank_factor_fibers line 31