OAI/Analysis/KadisonKastler/MinimalFamilyQuantity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Norm minimization may be performed on the invariant family itself. This lets us use the uniquely defined cyclic right factor without extending that factor to maps outside the family.

  1. theorem OAI.KadisonKastler.minimal_row_family_quantity_constant_on line 16