OAI/Combinatorics/SumProduct/Alignment/RationalEchelon02.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalMatrix.real line 26
  2. lemma OAI.RationalMatrix.real_apply line 30
  3. lemma OAI.RationalMatrix.real_single line 34
  4. lemma OAI.RationalMatrix.real_rat line 39
  5. lemma OAI.RationalMatrix.real_comp line 46
  6. lemma OAI.RationalMatrix.real_id line 54
  7. lemma OAI.RationalMatrix.real_sub line 60
  8. lemma OAI.RationalMatrix.real_injective line 65
  9. lemma OAI.RationalMatrix.real_injective_of_injective line 73
  10. def OAI.RationalEchelon.Chart.coords line 85
  11. lemma OAI.RationalEchelon.Chart.coords_embed line 90
  12. lemma OAI.RationalEchelon.Chart.embed_coords line 94
  13. lemma OAI.RationalEchelon.Chart.real_coords line 98
  14. lemma OAI.RationalEchelon.Chart.real_at_pivot line 102
  15. lemma OAI.RationalEchelon.Chart.coeff_zero line 106
  16. lemma OAI.RationalEchelon.Chart.real_prefix line 114
  17. def OAI.RationalEchelon.Chart.normal line 126
  18. lemma OAI.RationalEchelon.Chart.normal_apply line 128
  19. lemma OAI.RationalEchelon.Chart.normal_pivot line 130
  20. lemma OAI.RationalEchelon.Chart.normal_sub line 133
  21. lemma OAI.RationalEchelon.Chart.normal_eq_zero_iff line 136
  22. lemma OAI.RationalEchelon.Chart.real_normal line 143
  23. lemma OAI.RationalEchelon.Chart.real_normal_pivot line 150
  24. lemma OAI.RationalEchelon.Chart.real_normal_tail line 155
  25. def OAI.RationalMatrix.select line 180
  26. lemma OAI.RationalMatrix.real_select line 184
  27. def OAI.RationalEchelon.Chart.freeSet line 192
  28. def OAI.RationalEchelon.Chart.free line 193
  29. lemma OAI.RationalEchelon.Chart.free_ne_pivot line 195
  30. lemma OAI.RationalEchelon.Chart.pivot_or_free line 199
  31. def OAI.RationalEchelon.Chart.sectionMap line 210
  32. def OAI.RationalEchelon.Chart.quotientMap line 213
  33. lemma OAI.RationalEchelon.Chart.section_apply line 216
  34. lemma OAI.RationalEchelon.Chart.section_free line 220
  35. lemma OAI.RationalEchelon.Chart.section_pivot line 224
  36. lemma OAI.RationalEchelon.Chart.normal_section line 231
  37. lemma OAI.RationalEchelon.Chart.quotient_section line 235
  38. lemma OAI.RationalEchelon.Chart.section_quotient line 241
  39. lemma OAI.RationalEchelon.Chart.quotient_eq_zero_iff line 248
  40. lemma OAI.RationalEchelon.Chart.remainder_mem line 257
  41. lemma OAI.RationalEchelon.Chart.real_quotient line 261
  42. lemma OAI.RationalEchelon.Chart.real_section_free line 266
  43. lemma OAI.RationalEchelon.Chart.real_section_pivot line 270
  44. lemma OAI.RationalEchelon.Chart.real_quotient_section line 274
  45. lemma OAI.RationalEchelon.Chart.real_section_quotient line 281
  46. lemma OAI.RationalEchelon.Chart.real_normal_level line 288
  47. lemma OAI.RationalEchelon.Chart.real_quotient_level line 299
  48. lemma OAI.RationalEchelon.Chart.real_section_level line 306
  49. lemma OAI.RationalEchelon.Chart.section_map_injective line 317
  50. lemma OAI.RationalEchelon.Chart.map_section_quotient line 328
  51. lemma OAI.RationalEchelon.Chart.real_map_section_quotient line 335
  52. lemma OAI.RationalEchelon.Chart.real_kernel_iff line 344