OAI/Analysis/KadisonKastler/FiniteBlockTraceLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized sizes of equal matrix blocks

  1. theorem OAI.KadisonKastler.tendsto_finiteBlock_ratio line 13