OAI/Combinatorics/Progressions/Lattices/LieSubalgebraLatticeInnerGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.integralVector_mulVec_of_column_denominators line 12
2. theorem OAI.Erdos3.scaledIntegerGrid_mulVec_of_column_denominators line 27
3. theorem OAI.Erdos3.bchSubgroup_comap_inner_grid_of_columns line 35
4. theorem OAI.Erdos3.lieSubalgebra_comap_inner_grid_of_columns line 58
5. theorem OAI.Erdos3.NilpotentLieBCHGroup.realification_comap_incl_mem line 78
6. theorem OAI.Erdos3.NilpotentLieBCHGroup.realification_comap_incl_map_le line 92