OAI/Combinatorics/HadwigerCounterexample/BinaryMatrices.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Binary Matrices

  1. abbrev OAI.HadwigerCounterexample.F line 17
  2. abbrev OAI.HadwigerCounterexample.Vec line 18
  3. abbrev OAI.HadwigerCounterexample.Mat line 19
  4. abbrev OAI.HadwigerCounterexample.Space line 20
  5. theorem OAI.HadwigerCounterexample.bit_cases line 22
  6. theorem OAI.HadwigerCounterexample.bit_sq line 24
  7. theorem OAI.HadwigerCounterexample.char_two line 25
  8. theorem OAI.HadwigerCounterexample.odd_smul_bit line 27
  9. def OAI.HadwigerCounterexample.evmat line 35
  10. def OAI.HadwigerCounterexample.mpair line 37
  11. theorem OAI.HadwigerCounterexample.mpair_comm line 43
  12. theorem OAI.HadwigerCounterexample.mpair_outer line 47
  13. def OAI.HadwigerCounterexample.liftM line 53

    Source documentation

    Apply frame maps to the two factors of every tensor.

    def liftM (P : Mat K I) (Q : Mat L J) : Mat I J →ₗ[F] Mat K L where
…

    Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.F

  14. theorem OAI.HadwigerCounterexample.liftM_def line 58
  15. theorem OAI.HadwigerCounterexample.liftM_outer line 61
  16. theorem OAI.HadwigerCounterexample.liftM_comp line 67
  17. theorem OAI.HadwigerCounterexample.mpair_liftM line 72
  18. theorem OAI.HadwigerCounterexample.mat_left_inv line 96
  19. theorem OAI.HadwigerCounterexample.liftM_inj line 109