OAI/Analysis/KadisonKastler/TomitaResolventEndpoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absence of endpoint eigenvectors for the Tomita resolvent

  1. theorem OAI.KadisonKastler.one_sub_graphResolvent_eq_zero_iff line 14