OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare01.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LeibmanSquare.level_normal line 16
  2. def OAI.LeibmanSquare.level line 26
  3. lemma OAI.LeibmanSquare.mem_level line 42
  4. lemma OAI.LeibmanSquare.level_antitone line 46
  5. lemma OAI.LeibmanSquare.commutator_mem_level line 51
  6. def OAI.LeibmanSquare.filtration line 85
  7. lemma OAI.LeibmanSquare.level_zero line 91
  8. lemma OAI.LeibmanSquare.last_level line 97
  9. lemma OAI.LeibmanSquare.last_central line 108
  10. def OAI.LeibmanSquare.restricted line 122
  11. lemma OAI.LeibmanSquare.restricted_zero line 135
  12. lemma OAI.LeibmanSquare.restricted_one line 142
  13. lemma OAI.LeibmanSquare.last_normal line 151
  14. def OAI.LeibmanSquare.mapFiltration line 164
  15. theorem OAI.LeibmanSquare.quotient_lowers_degree line 176
  16. def OAI.LeibmanSquare.pairConj line 195
  17. lemma OAI.LeibmanSquare.conjugate_mod_next line 198
  18. lemma OAI.LeibmanSquare.pairConj_mem line 207
  19. lemma OAI.LeibmanSquare.pairConj_last_fixed line 221
  20. lemma OAI.LeibmanSquare.pairConj_lattice line 236
  21. lemma OAI.LeibmanSquare.orbit_normalization line 243
  22. def OAI.LeibmanSquare.diff line 256
  23. def OAI.LeibmanSquare.iterDiff line 258
  24. def OAI.LeibmanSquare.Polynomial line 264
  25. lemma OAI.LeibmanSquare.iterDiff_append line 267
  26. lemma OAI.LeibmanSquare.iterDiff_shift line 273
  27. lemma OAI.LeibmanSquare.iterDiff_hom line 286
  28. lemma OAI.LeibmanSquare.iterDiff_pair line 298
  29. theorem OAI.LeibmanSquare.polynomial_pair line 306
  30. lemma OAI.LeibmanSquare.iterDiff_left_mul line 316
  31. def OAI.LeibmanSquare.normalizedPair line 328
  32. theorem OAI.LeibmanSquare.normalizedPair_polynomial line 335
  33. lemma OAI.LeibmanSquare.polynomial_map line 355
  34. lemma OAI.LeibmanSquare.polynomial_filtered_map line 363
  35. def OAI.LeibmanSquare.restrictedConj line 373
  36. lemma OAI.LeibmanSquare.restrictedConj_filtered line 378
  37. theorem OAI.LeibmanSquare.normalized_conjugate_polynomial line 387
  38. theorem OAI.LeibmanSquare.reduced_pair_polynomial line 396