OAI/Analysis/KadisonKastler/MinimalFamilyDiagonalNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Diagonal norm preservation on a minimal row family. Central support localization handles arbitrary centers and represented multiplicities.

  1. theorem OAI.KadisonKastler.minimal_row_family_diagonal_norm line 19