OAI/Combinatorics/Progressions/Estimates/CubicSevenCornerSymmetry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_diagonal_expansion line 11
  2. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalDerivative line 88
  3. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven line 92
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalDerivative_norm line 95
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_norm line 101
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicDiagonalDerivative_unit line 106
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_unit line 111
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubic_diagonal_derivative_equivalence line 119
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_explicit line 172
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_replica_reduction line 184