OAI/Combinatorics/Progressions/Estimates/PrimitiveExtension.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BohrLattice.Primitive.IsPrimitive line 13
  2. theorem OAI.Erdos3.BohrLattice.Primitive.IsPrimitive.ne_zero line 16
  3. def OAI.Erdos3.BohrLattice.Primitive.content line 20
  4. theorem OAI.Erdos3.BohrLattice.Primitive.content_dvd line 22
  5. theorem OAI.Erdos3.BohrLattice.Primitive.content_ne_zero line 25
  6. def OAI.Erdos3.BohrLattice.Primitive.divideContent line 29
  7. theorem OAI.Erdos3.BohrLattice.Primitive.content_mul_divideContent line 31
  8. theorem OAI.Erdos3.BohrLattice.Primitive.exists_bezout_finset line 37
  9. theorem OAI.Erdos3.BohrLattice.Primitive.isPrimitive_of_content_eq_one line 68
  10. theorem OAI.Erdos3.BohrLattice.Primitive.divideContent_primitive line 75
  11. theorem OAI.Erdos3.BohrLattice.Primitive.divideContent_ne_zero line 85
  12. def OAI.Erdos3.BohrLattice.PrimitiveExtension.dotLinear line 98
  13. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.dotLinear_apply line 108
  14. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.isPrimitive_of_minimal_gauge line 111
  15. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.exists_basis_zero_eq_of_isPrimitive line 146
  16. def OAI.Erdos3.BohrLattice.PrimitiveExtension.zspanCoordEquiv line 185
  17. def OAI.Erdos3.BohrLattice.PrimitiveExtension.zspanBasis line 190
  18. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.zspanBasis_apply_coe line 195
  19. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.zspanCoordEquiv_apply line 200
  20. theorem OAI.Erdos3.BohrLattice.PrimitiveExtension.shortest_zspan_vector_primitive_and_extends line 206