OAI/Analysis/KadisonKastler/DerivationIdealImplementer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bringing an ideal-extension implementer into the unital algebra

In Sakai's unital specialization, an implementer in an extension can be multiplied by the original unit. If this product lies in the original algebra, it implements the same derivation.

  1. theorem OAI.KadisonKastler.inner_derivation_of_ideal_implementer line 18