OAI/Combinatorics/Progressions/Estimates/QuarticDiagonalWrap.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_diagonal_expansion line 12
  2. abbrev OAI.Erdos3.QuarticNonconstantCorner line 52
  3. theorem OAI.Erdos3.quarticNonconstantCorner_card line 54
  4. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalDerivative line 61
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMixedFifteen line 65
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalDerivative_norm line 69
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMixedFifteen_norm line 74
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalDerivative_unit line 79
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMixedFifteen_unit line 84
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_diagonal_derivative_equivalence line 92
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRoot line 153
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRoot_dim line 158
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_explicit_quartic_root_equivalence line 162
  14. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalDerivative line 220
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalDerivative_norm line 225
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalDerivative_unit line 231
  17. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticWrappedDiagonalDerivative line 237
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalWrapCoefficient line 241
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticWrappedDiagonalDerivative_norm line 245
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalWrapCoefficient_norm line 250
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticWrappedDiagonalDerivative_resolution line 255
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalDerivative_branches line 275
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticDiagonalWrapCoefficient_expansion line 294