OAI/Combinatorics/SumProduct/Alignment/AllLevel01.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegerHyperplane.split_prefix_zero_iff line 15
  2. lemma OAI.TailCharacterRechart.chart_early_zero_iff line 63
  3. lemma OAI.TailCharacterRechart.chart_late_zero_iff line 73
  4. lemma OAI.TailCharacterRechart.tail_of_mem line 113
  5. lemma OAI.TailCharacterRechart.chart_kernel line 126
  6. lemma OAI.TailCharacterRechart.pivot_lt_of_kills line 155
  7. theorem OAI.TailCharacterRechart.exists_refined_integer_cover line 179
  8. def OAI.AllLevelFactorization.shrinkLevel line 267
  9. lemma OAI.AllLevelFactorization.shrinkLevel_le line 270
  10. lemma OAI.AllLevelFactorization.shrinkLevel_le_one line 277
  11. lemma OAI.AllLevelFactorization.shrinkLevel_antitone line 282
  12. lemma OAI.AllLevelFactorization.shrinkLevel_commutator line 292
  13. def OAI.AllLevelFactorization.shrink line 323
  14. lemma OAI.AllLevelFactorization.shrink_zero_one line 328
  15. lemma OAI.AllLevelFactorization.shrink_at line 334
  16. lemma OAI.AllLevelFactorization.shrink_other line 337
  17. def OAI.AllLevelFactorization.levelKernel line 350
  18. lemma OAI.AllLevelFactorization.levelKernel_le line 352
  19. lemma OAI.AllLevelFactorization.mem_levelKernel line 356
  20. lemma OAI.AllLevelFactorization.next_le_levelKernel line 365
  21. lemma OAI.AllLevelFactorization.brackets_le_levelKernel line 370
  22. def OAI.AllLevelFactorization.kernelFiltration line 379
  23. lemma OAI.AllLevelFactorization.word_node_cutoff line 387
  24. lemma OAI.AllLevelFactorization.word_node line 399
  25. lemma OAI.AllLevelFactorization.coefficients_eq_of_initial line 403
  26. theorem OAI.AllLevelFactorization.corrected_taylor_coefficients line 416
  27. lemma OAI.AllLevelFactorization.word_mem_subgroup line 435
  28. lemma OAI.AllLevelFactorization.commutator_next line 448
  29. lemma OAI.AllLevelFactorization.conjugate_mem line 452
  30. lemma OAI.AllLevelFactorization.character_conjugate line 460
  31. lemma OAI.AllLevelFactorization.character_correction line 471
  32. theorem OAI.AllLevelFactorization.one_level_descent line 496
  33. theorem OAI.AllLevelFactorization.corrected_polynomial line 541