OAI/Probability/InvariantIsing/Core/FiniteFieldMatching.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Match as many sites of each field label as both finite populations contain.

  1. def OAI.InvariantIsing.fieldLabelInjection line 11
  2. lemma OAI.InvariantIsing.fieldLabelInjection_label line 35
  3. theorem OAI.InvariantIsing.exists_field_label_matching line 41