OAI/Analysis/KadisonSimilarity/FreeProduct/LeadingWordGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complement of the words starting in one factor consists exactly of the nonempty words starting in the other factor.

  1. theorem OAI.KadisonSimilarity.orthogonal_eq_of_dense_sup line 13
  2. theorem OAI.KadisonSimilarity.centeredFreeWordSpan_le_sides line 45
  3. theorem OAI.KadisonSimilarity.centeredWordSpace_orthogonal line 62