OAI/Analysis/KadisonKastler/HilbertSumConjugateClosure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fiber closure after a unitary change of coordinates

  1. theorem OAI.KadisonKastler.ae_hilbertSum_field_mem_of_conjugate_closure line 25
  2. theorem OAI.KadisonKastler.ae_hilbertSum_representation_field_mem line 40