OAI/Combinatorics/SumProduct/Alignment/RationalLattice23.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SourceIntegerArrays.source_compact_factorized_haar line 28
2. lemma OAI.RationalLattice.rationalHom_of_basis line 148
3. lemma OAI.RationalLattice.rationalHom_of_lattice line 176
4. lemma OAI.RationalLattice.rational_of_pos_pow line 195
5. lemma OAI.RationalLattice.CoveredLattice.mem_rational line 207
6. lemma OAI.RationalLattice.rationalHom_covered line 223
7. theorem OAI.SourceIntegerArrays.GlobalJoint.target_geometry line 250