OAI/Analysis/KadisonKastler/SimpleDerivationConstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Innerness of bounded derivations of simple unital C-star algebras

The maximal simple extension, extreme Hermitian separator, spatial factor splitting and faithful-corner norm argument together prove the precise unital input used in the stability application.

  1. theorem OAI.KadisonKastler.simple_extension_implementer_mem_range line 28
  2. theorem OAI.KadisonKastler.antiStar_derivation_inner_of_simple line 77
  3. theorem OAI.KadisonKastler.publishedSimpleDerivationInner line 90