OAI/Analysis/KadisonKastler/FiniteModuleObstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absence of a module map in a compact family has finitely many uniformly nonzero coefficient witnesses.

  1. theorem OAI.KadisonKastler.finite_sum_norm_pos line 15
  2. theorem OAI.KadisonKastler.compact_finite_module_obstruction line 23