OAI/Topology/HahnSeries/Pivots.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HahnWilson.PivotTopology.poleLattice line 15
  2. def OAI.HahnWilson.PivotTopology.monomial line 21
  3. def OAI.HahnWilson.PivotTopology.PreservesPoles line 23
  4. def OAI.HahnWilson.PivotTopology.matrixOf line 26
  5. def OAI.HahnWilson.PivotTopology.HasLeadingTerm line 29
  6. def OAI.HahnWilson.PivotTopology.HasLeadingPosition line 32
  7. def OAI.HahnWilson.PivotTopology.crossing line 35
  8. def OAI.HahnWilson.PivotTopology.crossingQuotient line 38
  9. instance OAI.HahnWilson.PivotTopology.crossingQuotient_addCommGroup line 43
  10. instance OAI.HahnWilson.PivotTopology.crossingQuotient_module line 48
  11. lemma OAI.HahnWilson.PivotTopology.mem_poleLattice line 53
  12. lemma OAI.HahnWilson.PivotTopology.poleLattice_mono line 56
  13. lemma OAI.HahnWilson.PivotTopology.coeff_monomial line 61
  14. lemma OAI.HahnWilson.PivotTopology.monomial_mem line 65
  15. lemma OAI.HahnWilson.PivotTopology.exists_poleLattice line 69
  16. lemma OAI.HahnWilson.PivotTopology.matrixOf_triangular line 74
  17. def OAI.HahnWilson.PivotTopology.truncate line 79
  18. lemma OAI.HahnWilson.PivotTopology.coeff_truncate line 82
  19. lemma OAI.HahnWilson.PivotTopology.truncate_mem line 88
  20. lemma OAI.HahnWilson.PivotTopology.sub_truncate_mem line 92
  21. def OAI.HahnWilson.PivotTopology.poleProjection line 100
  22. lemma OAI.HahnWilson.PivotTopology.poleProjection_eq_zero line 105
  23. lemma OAI.HahnWilson.PivotTopology.poleProjection_monomial_image line 117
  24. lemma OAI.HahnWilson.PivotTopology.poleProjection_truncate_image line 121
  25. lemma OAI.HahnWilson.PivotTopology.columnSpace_eq_projectedImage line 129
  26. lemma OAI.HahnWilson.PivotTopology.increment_zero_iff_finite_solution line 145
  27. lemma OAI.HahnWilson.PivotTopology.mem_poleLattice_iff_valuation line 171
  28. lemma OAI.HahnWilson.PivotTopology.poleLattice_eq_ball line 180
  29. lemma OAI.HahnWilson.PivotTopology.isClosed_poleLattice line 190
  30. lemma OAI.HahnWilson.PivotTopology.isOpen_poleLattice line 194
  31. lemma OAI.HahnWilson.PivotTopology.poleLattice_nhds_basis line 200
  32. lemma OAI.HahnWilson.PivotTopology.continuous_of_preservesPoles line 227
  33. lemma OAI.HahnWilson.PivotTopology.continuous_of_bounded_coefficients line 234
  34. def OAI.HahnWilson.PivotTopology.stageSeries line 256
  35. lemma OAI.HahnWilson.PivotTopology.coeff_stageSeries line 263
  36. lemma OAI.HahnWilson.PivotTopology.stageSeries_mem line 266
  37. lemma OAI.HahnWilson.PivotTopology.range_stageSeries line 270
  38. lemma OAI.HahnWilson.PivotTopology.continuous_stageSeries line 286
  39. lemma OAI.HahnWilson.PivotTopology.isCompact_poleLattice line 295
  40. lemma OAI.HahnWilson.PivotTopology.isCompact_leadingTerm line 301
  41. lemma OAI.HahnWilson.PivotTopology.isClosed_leadingTerm line 307
  42. lemma OAI.HahnWilson.PivotTopology.unmatched_iff_increments_zero line 313
  43. theorem OAI.HahnWilson.PivotTopology.unmatched_iff_kernel line 332
  44. lemma OAI.HahnWilson.PivotTopology.rowRank_step line 365
  45. lemma OAI.HahnWilson.PivotTopology.matchedRow_iff_unequal_ranks line 373
  46. lemma OAI.HahnWilson.PivotTopology.exists_rowCut_kernel_of_unequal_ranks line 398
  47. theorem OAI.HahnWilson.PivotTopology.matched_row_iff_image line 434
  48. def OAI.HahnWilson.PivotTopology.stageImage line 470
  49. lemma OAI.HahnWilson.PivotTopology.stageImage_mono line 473
  50. lemma OAI.HahnWilson.PivotTopology.stageImage_le_poleLattice line 477
  51. lemma OAI.HahnWilson.PivotTopology.stageImage_step line 482
  52. lemma OAI.HahnWilson.PivotTopology.monomial_image_mem_iff_unmatched line 501
  53. def OAI.HahnWilson.PivotTopology.imageModulo line 519
  54. lemma OAI.HahnWilson.PivotTopology.imageModulo_mono line 523
  55. lemma OAI.HahnWilson.PivotTopology.imageModulo_zero line 526
  56. lemma OAI.HahnWilson.PivotTopology.imageModulo_step line 532
  57. lemma OAI.HahnWilson.PivotTopology.imageModulo_finite line 538
  58. lemma OAI.HahnWilson.PivotTopology.mem_imageModulo line 550
  59. lemma OAI.HahnWilson.PivotTopology.imageModulo_finrank_step line 558
  60. lemma OAI.HahnWilson.PivotTopology.imageModulo_finrank line 573
  61. lemma OAI.HahnWilson.PivotTopology.matched_le line 592
  62. def OAI.HahnWilson.PivotTopology.columnMatches line 599
  63. def OAI.HahnWilson.PivotTopology.crossingStageMatches line 602
  64. lemma OAI.HahnWilson.PivotTopology.columnMatches_snd_inj line 605
  65. lemma OAI.HahnWilson.PivotTopology.columnMatches_finite line 612
  66. lemma OAI.HahnWilson.PivotTopology.columnMatches_ncard line 617
  67. lemma OAI.HahnWilson.PivotTopology.columnMatches_partition line 635
  68. lemma OAI.HahnWilson.PivotTopology.imageModulo_finrank_partition line 668
  69. lemma OAI.HahnWilson.PivotTopology.stageImage_le_ker_projection line 675
  70. def OAI.HahnWilson.PivotTopology.quotientProjection line 682
  71. lemma OAI.HahnWilson.PivotTopology.quotientProjection_mkQ line 687
  72. def OAI.HahnWilson.PivotTopology.crossingStage line 691
  73. lemma OAI.HahnWilson.PivotTopology.crossingStage_mono line 695
  74. lemma OAI.HahnWilson.PivotTopology.crossingStage_finite line 699
  75. lemma OAI.HahnWilson.PivotTopology.crossingStage_eq_inf line 705
  76. lemma OAI.HahnWilson.PivotTopology.quotientProjection_stage_range line 717
  77. lemma OAI.HahnWilson.PivotTopology.crossingStage_finrank line 729
  78. def OAI.HahnWilson.PivotTopology.crossingSpace line 745
  79. lemma OAI.HahnWilson.PivotTopology.crossingStage_le_space line 749
  80. lemma OAI.HahnWilson.PivotTopology.crossingSpace_stabilizes line 756
  81. def OAI.HahnWilson.PivotTopology.crossingQuotientEquiv line 783
  82. theorem OAI.HahnWilson.PivotTopology.crossing_dimension line 792
  83. lemma OAI.HahnWilson.PivotTopology.range_inf_stabilizes line 804
  84. lemma OAI.HahnWilson.PivotTopology.isCompact_range_inter_poleLattice line 821
  85. theorem OAI.HahnWilson.PivotTopology.closed_image line 833