OAI/Analysis/KadisonKastler/ProductBicentralizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bicentralizer reduction along the fixed product leg

The independent finite-site swaps give a trivial bicentralizer for the product vector. In a tensor product the same exact centralizer tests force every bicentralizer element into the first tensor leg. Triviality of that leg is a separate hypothesis.

  1. theorem OAI.KadisonKastler.ProductMatrixStages.bicentralizer_scalar line 26
  2. theorem OAI.KadisonKastler.spatial_bicentralizer_mem_left line 36