OAI/Combinatorics/SumProduct/Alignment/MalcevTail01.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MalcevHorizontal.character_lower_trivial line 30
  2. lemma OAI.MalcevHorizontal.original_horizontal_linear line 36
  3. theorem OAI.MalcevHorizontal.original_horizontal_obstruction line 47
  4. lemma OAI.MalcevHorizontal.horizontal_pow line 89
  5. lemma OAI.MalcevHorizontal.representative_torus line 103
  6. lemma OAI.MalcevHorizontal.reduced_horizontal_bound line 118
  7. lemma OAI.MalcevHorizontal.canonical_representative_orbit line 129
  8. theorem OAI.MalcevHorizontal.geometric_scalar_descent line 162
  9. def OAI.MalcevTailSection.axisHom line 253
  10. def OAI.MalcevTailSection.HasPivot line 258
  11. def OAI.MalcevTailSection.tailSection line 262
  12. lemma OAI.MalcevTailSection.section_zero line 266
  13. lemma OAI.MalcevTailSection.section_add line 271
  14. def OAI.MalcevTailSection.flow line 277
  15. lemma OAI.MalcevTailSection.section_zpow line 283
  16. lemma OAI.MalcevTailSection.section_continuous line 288
  17. lemma OAI.MalcevTailSection.section_tail line 295
  18. lemma OAI.MalcevTailSection.section_rational line 308
  19. lemma OAI.MalcevTailSection.section_bound line 320
  20. lemma OAI.MalcevTailSection.form_zero_of_no_pivot line 335
  21. lemma OAI.MalcevTailSection.character_section line 349