OAI/Combinatorics/SumProduct/Alignment/TriangularDenominators01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CocompactLattice.closure_eq_top_of_nhds line 38
  2. lemma OAI.CocompactLattice.generating_intersection line 50
  3. theorem OAI.CocompactLattice.fg_of_compact_reps line 105
  4. def OAI.TriangularDenominators.HasDenom line 144
  5. lemma OAI.TriangularDenominators.denom_zero line 146
  6. lemma OAI.TriangularDenominators.denom_add line 147
  7. lemma OAI.TriangularDenominators.denom_neg line 152
  8. lemma OAI.TriangularDenominators.denom_mul line 155
  9. lemma OAI.TriangularDenominators.denom_mono line 161
  10. lemma OAI.TriangularDenominators.denom_self line 167
  11. lemma OAI.TriangularDenominators.finite_common_denom line 174
  12. theorem OAI.TriangularDenominators.polynomial_grid line 184
  13. structure OAI.TriangularDenominators.Coordinates line 208
  14. theorem OAI.TriangularDenominators.closure_grid line 218
  15. lemma OAI.TriangularDenominators.denom_small line 272
  16. theorem OAI.TriangularDenominators.closure_discrete line 288
  17. theorem OAI.TriangularDenominators.finiteIndex_of_compact_reps line 320