OAI/Probability/InvariantIsing/Cavity/CavityRationalRetained.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact finite group equivalences in the rational cavity coupling.

  1. def OAI.InvariantIsing.cavityRationalSize line 14
  2. def OAI.InvariantIsing.cavityRationalRetained line 16
  3. def OAI.InvariantIsing.cavityRationalFullGroup line 19
  4. lemma OAI.InvariantIsing.cavityRationalSize_ge_three line 24
  5. lemma OAI.InvariantIsing.cavityRationalRetained_full line 30
  6. def OAI.InvariantIsing.cavityRationalRetainedEquiv line 39
  7. def OAI.InvariantIsing.cavityRationalBaseEquiv line 47
  8. lemma OAI.InvariantIsing.cavityRationalBase_dimension line 54