OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal02.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MalcevHorizontal.character line 29
  2. lemma OAI.MalcevHorizontal.character_continuous line 37
  3. lemma OAI.MalcevHorizontal.character_basis line 42
  4. lemma OAI.MalcevHorizontal.character_ne_one line 48
  5. lemma OAI.MalcevHorizontal.character_injective line 58
  6. lemma OAI.MalcevHorizontal.character_integer line 69
  7. lemma OAI.MalcevHorizontal.matrix_entry line 84
  8. lemma OAI.MalcevHorizontal.column_character line 93
  9. lemma OAI.MalcevHorizontal.matrix_zero_iff line 104
  10. theorem OAI.MalcevHorizontal.nonzero_column line 120
  11. def OAI.MalcevHorizontal.squareMatrixBound line 143
  12. lemma OAI.MalcevHorizontal.squareMatrixBound_nonneg line 149
  13. lemma OAI.MalcevHorizontal.matrix_bound line 155
  14. def OAI.PolynomialCharacterDescent.shiftCoefficient line 185
  15. lemma OAI.PolynomialCharacterDescent.shiftCoefficient_eval line 188
  16. lemma OAI.PolynomialCharacterDescent.shiftCoefficient_degree line 193
  17. lemma OAI.PolynomialCharacterDescent.shiftCoefficient_coeff line 199
  18. lemma OAI.PolynomialCharacterDescent.choose_dvd_factorial line 203
  19. theorem OAI.PolynomialCharacterDescent.shift_coefficients line 212
  20. theorem OAI.PolynomialCharacterDescent.high_coefficients line 282
  21. theorem OAI.PolynomialCharacterDescent.nonlinear_coefficients line 293