OAI/Combinatorics/SumProduct/Alignment/RationalLattice27.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalLattice.QuotientLogImage.coordinates_mul line 22
2. lemma OAI.RationalLattice.QuotientLogImage.law_eq line 62
3. def OAI.RationalLattice.QuotientLogImage.imageChart line 72
4. lemma OAI.RationalLattice.QuotientLogImage.coordinates_adapted line 81
5. lemma OAI.RationalLattice.QuotientLogImage.imageChart_adapted line 97
6. def OAI.RationalLattice.QuotientLogImage.imageSecondChart line 102
7. lemma OAI.RationalLattice.QuotientLogImage.imageSecondChart_secondKind line 105
8. lemma OAI.RationalLattice.QuotientLogImage.imageSecondChart_adapted line 108
9. lemma OAI.RationalLattice.QuotientLogImage.imageEmbedding_polynomial line 119
10. lemma OAI.RationalLattice.QuotientLogImage.imageEmbedding_rational line 127
11. lemma OAI.RationalLattice.rationalInduced_discrete line 167
12. lemma OAI.RationalLattice.rationalInduced_compact_reps line 172
13. lemma OAI.RationalLattice.rationalInduced_compactSpace line 191
14. lemma OAI.RationalLattice.rationalConjugate_compact_reps line 202
15. lemma OAI.RationalLattice.rationalConjugate_compactSpace line 218
16. lemma OAI.RationalLattice.rationalConjugate_discrete line 232
17. lemma OAI.RationalLattice.rationalConjugate_ambient_discrete line 239
18. lemma OAI.RationalLattice.rationalConjugate_quotient_t2 line 246