OAI/Analysis/KadisonKastler/NestedMeanEquivariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Equivariance of nested means for separate group actions

  1. theorem OAI.KadisonKastler.scalarSeparatePullback line 22
  2. theorem OAI.KadisonKastler.nestedScalarMeanL_equivariant line 43
  3. def OAI.KadisonKastler.nestedScalarBoundaryMean line 66