OAI/Combinatorics/Progressions/Estimates/SymmetricSquarefreeMonotonicity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.tensorPower line 20
  2. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.reindex line 57
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_of_unit_data line 80
  4. def OAI.Erdos3.tensorIndexEquiv line 127
  5. def OAI.Erdos3.tensorPowerBudget line 130
  6. theorem OAI.Erdos3.tensorPowerBudget_bounds line 132
  7. def OAI.Erdos3.NativeMultidegreeNilcharacter.tensorPower line 150
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorPower_eval line 168
  9. def OAI.Erdos3.tensorVector line 183
  10. theorem OAI.Erdos3.product_flatten line 186
  11. def OAI.Erdos3.rootTensorEquiv line 193
  12. def OAI.Erdos3.rootTensorIndex line 199
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorPower_tensor_eval line 204
  14. theorem OAI.Erdos3.tensorVector_unit line 226
  15. structure OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData line 252
  16. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonVerticalProduct line 297
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonVerticalProduct_norm line 305
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_symmetric_squarefree_unit line 325
  19. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.eval line 416
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.eval_permute line 423
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.unit_eval line 436
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.norm_eval line 440
  23. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.mono line 462
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SymmetricSquarefreeUnitData.mono_eval line 469