OAI/Analysis/KadisonKastler/OrthogonalIdempotentIndependence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Independence of nonzero orthogonal idempotents

  1. theorem OAI.KadisonKastler.linearIndependent_of_orthogonal_idempotents line 12