OAI/Combinatorics/SumProduct/Alignment/RationalLattice09.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalLattice.coordinate_quotient_t2 line 29
2. lemma OAI.RationalLattice.coordinate_quotient_metrizable line 42
3. abbrev OAI.RationalLattice.coordinateQuotientMetric line 50
4. lemma OAI.RationalLattice.coordinateQuotientMetric_topology line 54
5. theorem OAI.AbelianMalcevTorus.quantitative_abelian_quotient_observable line 79
6. theorem OAI.SquareInduction.quadratic_eigenfunction_observable line 177