OAI/Analysis/KadisonKastler/FixedFiberFieldAgreement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compressed field agrees with the genuine fixed-fiber representation

  1. theorem OAI.KadisonKastler.compressedStratumField_eq_operator line 18
  2. theorem OAI.KadisonKastler.compressedStratumField_eq_fixedFiberRepresentation line 38