OAI/Combinatorics/Progressions/Lattices/SourceLatticeCover.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.withLattice line 11
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.withLattice_geometry line 19
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_image_cover line 29
  4. def OAI.Erdos3.RationalFilteredNilmanifold.lowerCoverLattice line 114
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.lowerCoverLattice_coordinates line 118
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.lowerCoverLattice_forward line 123
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.lowerCoverLattice_backward line 132
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.lowerCoverLattice_le line 139
  9. def OAI.Erdos3.RationalFilteredNilmanifold.loweredCover line 149
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCover_filtration line 154
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.loweredCover_geometry line 156
  12. theorem OAI.Erdos3.bchSubgroupCoordinates_comap_ofSteps line 172
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_source_cover line 190