OAI/Combinatorics/Progressions/Linear/SortedBasisTriangular.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.basis_reindex_equivFun line 12
  2. theorem OAI.Erdos3.basis_reindex_toMatrix line 19
  3. theorem OAI.Erdos3.basis_coordinate_linearEquiv_matrix line 27
  4. theorem OAI.Erdos3.realDenominatorGrid_comp line 42
  5. theorem OAI.Erdos3.basis_reindex_grid line 50
  6. theorem OAI.Erdos3.sorted_basis_upper_zero line 67
  7. theorem OAI.Erdos3.sorted_basis_diagonal_one line 76
  8. theorem OAI.Erdos3.sorted_basis_initial_identity line 84