OAI/Probability/ClassicalON/BondSigns.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.signFieldEquiv line 11
  2. theorem OAI.ClassicalON.signFieldEquiv_true line 19
  3. theorem OAI.ClassicalON.signFieldEquiv_false line 20
  4. def OAI.ClassicalON.fieldSign line 22
  5. theorem OAI.ClassicalON.signField_cases line 24
  6. theorem OAI.ClassicalON.fieldSign_zero line 27
  7. theorem OAI.ClassicalON.fieldSign_one line 28
  8. theorem OAI.ClassicalON.fieldSign_add line 30
  9. theorem OAI.ClassicalON.fieldSign_sq line 34
  10. def OAI.ClassicalON.compatibleSigns line 39
  11. def OAI.ClassicalON.compatibleSignsEquiv line 42
  12. theorem OAI.ClassicalON.compatibleSigns_card line 51
  13. theorem OAI.ClassicalON.compatibleSigns_sum line 57
  14. def OAI.ClassicalON.bondConnected line 64
  15. theorem OAI.ClassicalON.bondConnected_mono line 68
  16. theorem OAI.ClassicalON.bond_sign_correlation line 74