OAI/Combinatorics/SumProduct/Alignment/RationalLattice01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalLattice.IsRational line 17
  2. lemma OAI.RationalLattice.eval_rational line 20
  3. lemma OAI.RationalLattice.rational_one line 29
  4. lemma OAI.RationalLattice.rational_mul line 33
  5. lemma OAI.RationalLattice.rational_inv line 44
  6. def OAI.RationalLattice.rationalSubgroup line 70
  7. def OAI.RationalLattice.qcoord line 76
  8. lemma OAI.RationalLattice.qcoord_spec line 79
  9. lemma OAI.RationalLattice.qcoord_injective line 82
  10. lemma OAI.RationalLattice.qcoord_continuous line 89
  11. def OAI.RationalLattice.rationalCoordinates line 96
  12. theorem OAI.RationalLattice.rational_fg_discrete line 123
  13. theorem OAI.RationalLattice.finite_rational_extension line 140
  14. lemma OAI.Polynomial.exists_antidifference_monomial line 178
  15. theorem OAI.Polynomial.exists_antidifference line 193
  16. lemma OAI.Polynomial.exists_antidifference_monomial_algebra line 214
  17. theorem OAI.Polynomial.exists_antidifference_algebra line 234