OAI/Analysis/KadisonKastler/StateScalingCoisometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extending a modular partial isometry to a coisometry

In a diffuse factorial centralizer, a nonzero scaling partial isometry of ratio at most one can be cut and moved into a finite orthogonal partition of the identity. This is the finite construction needed for absorption.

  1. theorem OAI.KadisonKastler.exists_state_scaling_coisometry line 24