OAI/Geometry/PeriodicTiling/IntegerMatrixIndex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PeriodicTilingThree.integer_mulVec_mem_of_columns line 15
2. theorem OAI.PeriodicTilingThree.determinant_smul_mem_of_columns line 27
3. theorem OAI.PeriodicTilingThree.finiteIndex_of_integer_columns line 34
4. theorem OAI.PeriodicTilingThree.det_ne_zero_of_scaled_columns_basis line 58
5. theorem OAI.PeriodicTilingThree.lattice_pullback_finiteIndex line 77