OAI/Combinatorics/SumProduct/Alignment/IntegerHyperplane01.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntegerHyperplane.form line 24
  2. def OAI.IntegerHyperplane.generator line 30
  3. def OAI.IntegerHyperplane.realGenerator line 33
  4. lemma OAI.IntegerHyperplane.realGenerator_eq line 35
  5. lemma OAI.IntegerHyperplane.generator_mem line 41
  6. lemma OAI.IntegerHyperplane.decomposition line 47
  7. theorem OAI.IntegerHyperplane.kernel_span line 75
  8. lemma OAI.IntegerHyperplane.generator_bound line 90
  9. theorem OAI.IntegerHyperplane.form_surjective line 104
  10. theorem OAI.IntegerHyperplane.kernel_finrank line 115
  11. def OAI.IntegerHyperplane.lift line 139
  12. lemma OAI.IntegerHyperplane.lift_succAbove line 142
  13. lemma OAI.IntegerHyperplane.lift_pivot line 146
  14. lemma OAI.IntegerHyperplane.form_lift line 150
  15. lemma OAI.IntegerHyperplane.lift_remove line 159
  16. lemma OAI.IntegerHyperplane.lift_continuous line 174
  17. lemma OAI.IntegerHyperplane.lift_zero line 187
  18. lemma OAI.IntegerHyperplane.lift_polynomial line 191
  19. lemma OAI.IntegerHyperplane.lift_lower_dep line 218
  20. def OAI.RationalCharacterKernel.coordinates line 246
  21. lemma OAI.RationalCharacterKernel.form_coord_kernel line 249
  22. lemma OAI.RationalCharacterKernel.coord_lift line 256
  23. def OAI.RationalCharacterKernel.rebuild line 259
  24. lemma OAI.RationalCharacterKernel.coordinates_rebuild line 266
  25. lemma OAI.RationalCharacterKernel.rebuild_coordinates line 271
  26. lemma OAI.RationalCharacterKernel.coordinates_continuous line 278
  27. lemma OAI.RationalCharacterKernel.rebuild_continuous line 283
  28. def OAI.RationalCharacterKernel.kernelHomeomorph line 287
  29. lemma OAI.RationalCharacterKernel.exists_kernel_correction line 295
  30. def OAI.RationalCharacterKernel.kernelCorrection line 323
  31. lemma OAI.RationalCharacterKernel.kernel_mul_coord line 329
  32. def OAI.RationalCharacterKernel.kernelCoordinates line 360
  33. lemma OAI.RationalCharacterKernel.kernelCoordinates_rational line 366