OAI/RepresentationTheory/TensorSquares/Arithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Parity-compatible triangular degrees and remainder bounds.

  1. def OAI.UniversalTensorSquares.triangular line 12
  2. lemma OAI.UniversalTensorSquares.triangular_eq_staircase_card line 14
  3. lemma OAI.UniversalTensorSquares.triangular_zero line 17
  4. lemma OAI.UniversalTensorSquares.triangular_one line 18
  5. lemma OAI.UniversalTensorSquares.triangular_succ line 20
  6. lemma OAI.UniversalTensorSquares.index_le_triangular line 23
  7. lemma OAI.UniversalTensorSquares.triangular_add_three line 28
  8. def OAI.UniversalTensorSquares.largestIndex line 35
  9. lemma OAI.UniversalTensorSquares.largestIndex_spec line 38
  10. lemma OAI.UniversalTensorSquares.largestIndex_maximal line 48
  11. def OAI.UniversalTensorSquares.remainderPairs line 52
  12. lemma OAI.UniversalTensorSquares.degree_decomposition line 54
  13. lemma OAI.UniversalTensorSquares.odd_index_remainder_bound line 60
  14. lemma OAI.UniversalTensorSquares.even_index_remainder_bound line 72
  15. lemma OAI.UniversalTensorSquares.small_index_degree_bound line 84