OAI/Combinatorics/SumProduct/Alignment/RationalLattice25.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoveringSubspace.subgroup_orbit_covering line 19
  2. theorem OAI.CoveringSubspace.subgroup_path_mem line 43
  3. lemma OAI.CubeFaces.latticeArrays_isDiscrete line 59
  4. theorem OAI.CubeFaces.quotient_affine_face_displacement line 78
  5. lemma OAI.RationalLattice.chart_level_pathConnected line 137
  6. def OAI.RationalLattice.PreservesFaces line 146
  7. theorem OAI.RationalLattice.face_displacement_all_levels line 154
  8. theorem OAI.RationalLattice.face_affine_displacement_weighted line 178
  9. theorem OAI.RationalLattice.logHomLinear_level_map line 214
  10. theorem OAI.RationalLattice.logHomLinear_preserves line 240
  11. theorem OAI.RationalLattice.exists_face_lift line 272