OAI/Combinatorics/SumProduct/Alignment/RationalLattice20.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SourceIntegerArrays.joint_array_topology line 28
2. theorem OAI.SourceIntegerArrays.source_global_literal_cube_faces line 93
3. theorem OAI.RationalLattice.exists_joint_integer_sublattice line 218
4. def OAI.RationalLattice.conjugateEmbedding line 283
5. lemma OAI.RationalLattice.conjugateEmbedding_apply line 287
6. theorem OAI.RationalLattice.rational_conjugate_cover line 290