OAI/Combinatorics/SumProduct/Alignment/RationalLattice26.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalMatrix.real_polynomial line 22
2. lemma OAI.RationalMatrix.exists_matrix line 28
3. lemma OAI.RationalLattice.logHom_rational_polynomial line 61
4. theorem OAI.RationalLattice.exists_log_matrix line 74
5. def OAI.RationalLattice.QuotientLogImage.parametrization line 106
6. lemma OAI.RationalLattice.QuotientLogImage.parametrization_exp line 110
7. lemma OAI.RationalLattice.QuotientLogImage.parametrization_quotient line 118
8. lemma OAI.RationalLattice.QuotientLogImage.parametrization_embedding line 129
9. lemma OAI.RationalLattice.QuotientLogImage.parametrization_surjective line 140
10. def OAI.RationalLattice.QuotientLogImage.coordinates line 149
11. lemma OAI.RationalLattice.QuotientLogImage.coordinates_symm line 153
12. lemma OAI.RationalLattice.QuotientLogImage.coordinates_map line 156
13. lemma OAI.RationalLattice.QuotientLogImage.coordinates_one line 162
14. theorem OAI.RationalLattice.QuotientLogImage.image_isClosed line 168
15. lemma OAI.RationalLattice.QuotientLogImage.parametrization_polynomial line 189
16. def OAI.RationalLattice.QuotientLaw.multiply line 216
17. lemma OAI.RationalLattice.QuotientLaw.multiply_left line 222
18. lemma OAI.RationalLattice.QuotientLaw.multiply_right line 228
19. lemma OAI.RationalLattice.QuotientLaw.multiply_polynomial line 235
20. lemma OAI.RationalLattice.QuotientLaw.quotient_preserves line 252
21. lemma OAI.RationalLattice.QuotientLaw.section_preserves line 256
22. lemma OAI.RationalLattice.QuotientLaw.multiply_weighted line 262