OAI/Analysis/KadisonKastler/HilbertSumFieldTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Moving an operator-field model through its Hilbert coordinates

  1. theorem OAI.KadisonKastler.transported_algebra_field_decompose line 22
  2. theorem OAI.KadisonKastler.transported_commutant_fields_of_field_inclusion line 39