OAI/Combinatorics/Progressions/Estimates/QuarticFrozenRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.quarticBlockSample_input line 11
  2. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHnnnTensor line 42
  3. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhnnTensor line 45
  4. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhhnTensor line 48
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHnnnTensor_norm line 51
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhnnTensor_norm line 56
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhhnTensor_norm line 61
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHnnnTensor_unit line 66
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhnnTensor_unit line 70
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticHhhnTensor_unit line 74
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSymmetricFifteen_merge line 78
  12. abbrev OAI.Erdos3.QuarticMiddleIndex line 123
  13. def OAI.Erdos3.quarticGroupedFifteenMerge line 125
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMiddleTensor line 133
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMiddleTensor_norm line 136
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMiddleTensor_unit line 142
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSymmetricFifteen_grouped_merge line 147
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_original_root_equivalence line 165
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_hhnn_row_expansion line 219
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticHhnnTensor_row_expansion line 249
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_hhhn_row_expansion line 269
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticHhhnTensor_row_expansion line 299
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticMiddleTensor_row_expansion line 319