OAI/NumberTheory/PiExponent/Approximation/MatrixTranslation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.MatrixTranslation.periodCoordinate line 12
  2. def OAI.PiExponent.MatrixTranslation.periodMonomial line 15
  3. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_as_shift line 20
  4. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_coeff line 27
  5. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_support_le line 38
  6. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_support_weight line 52
  7. def OAI.PiExponent.MatrixTranslation.transverseIndices line 63
  8. theorem OAI.PiExponent.MatrixTranslation.mem_transverseIndices line 67
  9. theorem OAI.PiExponent.MatrixTranslation.card_transverseIndices line 74
  10. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_support_subset line 78
  11. theorem OAI.PiExponent.MatrixTranslation.transverseIndices_coordinate_le line 86
  12. theorem OAI.PiExponent.MatrixTranslation.transverseIndices_card_le line 98
  13. theorem OAI.PiExponent.MatrixTranslation.row_term_count line 113
  14. def OAI.PiExponent.MatrixTranslation.formalMonomialImage line 123
  15. theorem OAI.PiExponent.MatrixTranslation.coordinate_translation line 129
  16. theorem OAI.PiExponent.MatrixTranslation.periodMonomial_shift line 139
  17. theorem OAI.PiExponent.MatrixTranslation.formalMonomialImage_coeff line 156
  18. theorem OAI.PiExponent.MatrixTranslation.matrix_entry_translation line 163
  19. theorem OAI.PiExponent.MatrixTranslation.matrix_entry_translation_choices line 176
  20. theorem OAI.PiExponent.MatrixTranslation.det_dependent_row_sum line 195
  21. theorem OAI.PiExponent.MatrixTranslation.det_matrix_translation line 214