OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal01.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IntegralBilinear.V line 24
  2. def OAI.IntegralBilinear.basisVector line 26
  3. lemma OAI.IntegralBilinear.basis_expansion line 28
  4. def OAI.IntegralBilinear.leftHom line 33
  5. lemma OAI.IntegralBilinear.continuous_left line 38
  6. lemma OAI.IntegralBilinear.continuous_right line 42
  7. lemma OAI.IntegralBilinear.coordinate_expansion line 46
  8. theorem OAI.IntegralBilinear.integer_matrix line 75
  9. theorem OAI.IntegralBilinear.alternating_integer_matrix line 96
  10. def OAI.IntegralBilinear.contraction line 120
  11. lemma OAI.IntegralBilinear.contraction_pairing line 123
  12. lemma OAI.IntegralBilinear.contraction_add line 128
  13. lemma OAI.IntegralBilinear.contraction_integer line 133
  14. lemma OAI.IntegralBilinear.lattice_correction line 139
  15. def OAI.MalcevHorizontal.horizontal line 164
  16. def OAI.MalcevHorizontal.coordSection line 168
  17. lemma OAI.MalcevHorizontal.horizontal_one line 171
  18. lemma OAI.MalcevHorizontal.continuous_horizontal line 175
  19. lemma OAI.MalcevHorizontal.continuous_section line 178
  20. lemma OAI.MalcevHorizontal.horizontal_section line 186
  21. lemma OAI.MalcevHorizontal.section_zero line 191
  22. lemma OAI.MalcevHorizontal.horizontal_mul line 199
  23. lemma OAI.MalcevHorizontal.horizontal_inv line 204
  24. def OAI.MalcevHorizontal.quotientHom line 210
  25. lemma OAI.MalcevHorizontal.continuous_quotientHom line 215
  26. lemma OAI.MalcevHorizontal.pairing_eq_right line 223
  27. lemma OAI.MalcevHorizontal.pairing_eq_left line 233
  28. lemma OAI.MalcevHorizontal.pairing_projection line 238
  29. lemma OAI.MalcevHorizontal.section_add_pairing_left line 244
  30. lemma OAI.MalcevHorizontal.section_add_pairing_right line 254
  31. def OAI.MalcevHorizontal.bilinear line 266
  32. lemma OAI.MalcevHorizontal.bilinear_continuous line 290
  33. lemma OAI.MalcevHorizontal.integer_section line 304
  34. lemma OAI.MalcevHorizontal.bilinear_integer line 315
  35. theorem OAI.MalcevHorizontal.square_integer_matrix line 332