ExtremeDerivationFactor.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The factor lemma for an extreme derivation separator

This is the unital application of the factor lemma on p.261 of Sakai's 1971 paper. The signed cyclic representation is constructed separately; central projections commute with the spatial derivation implementer, so extremality forces them to be trivial.

theorem OAI.KadisonKastler.factor_of_extreme_signed_derivation_extension line 21