OAI/Analysis/KadisonKastler/DoubleGaussianConstant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constancy along the quotient of two commuting KMS actions

  1. theorem OAI.KadisonKastler.doubleGaussian_diagonal_coefficient_constant line 18