OAI/Combinatorics/Progressions/Estimates/DetectedTranslationMajorBase.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedGenerators line 21
  2. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedBaseMatrix line 25
  3. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedGenerators_span line 29
  4. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedBaseMatrix_span line 38
  5. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedBaseMatrix_real_image_eq_span line 47
  6. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedBaseMatrix_real_mem_span line 58
  7. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedGenerators_coordinate_logHeight line 78
  8. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedBaseMatrix_logHeight line 85
  9. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationProjectedGenerators_polynomial_logHeight line 90
  10. theorem OAI.Erdos3.PolynomialTranslationLie.residuePairProjectedGenerators_data line 109
  11. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_majorOrbitSymbol line 175
  12. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBase_span_eq_real_image line 195