OAI/Computability/MinUncut/Encoding/BinaryLinear.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Integration.BinaryLinear.F2 line 11
2. abbrev OAI.MinUncutGames.Integration.BinaryLinear.Vector line 12
3. def OAI.MinUncutGames.Integration.BinaryLinear.ofBit line 14
4. def OAI.MinUncutGames.Integration.BinaryLinear.toBit line 15
5. theorem OAI.MinUncutGames.Integration.BinaryLinear.scalar_cases line 17
6. theorem OAI.MinUncutGames.Integration.BinaryLinear.ofBit_toBit line 18
7. theorem OAI.MinUncutGames.Integration.BinaryLinear.toBit_ofBit line 19
8. theorem OAI.MinUncutGames.Integration.BinaryLinear.ofBit_xor line 20
9. theorem OAI.MinUncutGames.Integration.BinaryLinear.toBit_add line 21
10. def OAI.MinUncutGames.Integration.BinaryLinear.toVector line 23
11. def OAI.MinUncutGames.Integration.BinaryLinear.fromVector line 24
12. theorem OAI.MinUncutGames.Integration.BinaryLinear.toVector_fromVector line 26
13. theorem OAI.MinUncutGames.Integration.BinaryLinear.fromVector_toVector line 30
14. def OAI.MinUncutGames.Integration.BinaryLinear.coordinatesEquiv line 34
15. theorem OAI.MinUncutGames.Integration.BinaryLinear.toVector_xor line 40
16. theorem OAI.MinUncutGames.Integration.BinaryLinear.fromVector_add line 45
17. theorem OAI.MinUncutGames.Integration.BinaryLinear.toVector_zero line 49
18. theorem OAI.MinUncutGames.Integration.BinaryLinear.fromVector_zero line 54
19. def OAI.MinUncutGames.Integration.BinaryLinear.liftLinear line 57
20. theorem OAI.MinUncutGames.Integration.BinaryLinear.liftLinear_apply line 68
21. theorem OAI.MinUncutGames.Integration.BinaryLinear.finrank_vector line 73