OAI/Combinatorics/Progressions/Geometry/ControlledIntegralCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integralOrderedBasisProduct line 16
  2. theorem OAI.Erdos3.integralOrderedBasisProduct_eq_zpowProduct line 20
  3. theorem OAI.Erdos3.integral_basis_factor_mem line 33
  4. theorem OAI.Erdos3.integralOrderedBasisProduct_mem line 42
  5. theorem OAI.Erdos3.IsCentralLieBasis.integralOrderedBasisProduct_injective line 55
  6. theorem OAI.Erdos3.IsCentralLieBasis.exists_integralOrderedBasisProduct line 63
  7. def OAI.Erdos3.IsCentralLieBasis.integralOrderedBasisEquiv line 117
  8. theorem OAI.Erdos3.IsCentralLieBasis.exists_unique_integralOrderedBasisProduct line 127
  9. def OAI.Erdos3.realIntegralOrderedBasisProduct line 150
  10. theorem OAI.Erdos3.realification_integralOrderedBasisProduct line 155
  11. theorem OAI.Erdos3.realIntegralOrderedBasisProduct_mem line 171
  12. theorem OAI.Erdos3.IsCentralLieBasis.realIntegralOrderedBasisProduct_injective line 184
  13. theorem OAI.Erdos3.IsCentralLieBasis.exists_realIntegralOrderedBasisProduct line 191
  14. theorem OAI.Erdos3.IsCentralLieBasis.exists_unique_realIntegralOrderedBasisProduct line 202
  15. def OAI.Erdos3.IsCentralLieBasis.realIntegralOrderedBasisEquiv line 212
  16. theorem OAI.Erdos3.IsCentralLieBasis.mul_realIntegralOrderedBasisProduct_coordinate line 225
  17. theorem OAI.Erdos3.exists_controlled_integral_coordinates line 246