OAI/Combinatorics/SumProduct/Alignment/SquareHorizontal01.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalFactorPeriods.choosePolynomial line 24
  2. lemma OAI.RationalFactorPeriods.choosePolynomial_eval line 26
  3. lemma OAI.RationalFactorPeriods.choosePolynomial_int line 31
  4. lemma OAI.RationalFactorPeriods.choosePolynomial_natDegree line 36
  5. def OAI.RationalFactorPeriods.wordCharacterPolynomial line 42
  6. lemma OAI.RationalFactorPeriods.wordCharacterPolynomial_eval line 46
  7. lemma OAI.RationalFactorPeriods.wordCharacterPolynomial_degree line 54
  8. lemma OAI.LeibmanSquare.character_polynomial line 72
  9. lemma OAI.LeibmanSquare.remainder_character_polynomial line 86
  10. def OAI.SquareHorizontalCharacter.diagonal line 137
  11. def OAI.SquareHorizontalCharacter.lower line 143
  12. def OAI.SquareHorizontalCharacter.tail line 151
  13. lemma OAI.SquareHorizontalCharacter.split line 153
  14. theorem OAI.SquareHorizontalCharacter.character_split line 162
  15. lemma OAI.SquareHorizontalCharacter.lower_conj line 169
  16. lemma OAI.SquareHorizontalCharacter.commutator_mem line 182
  17. def OAI.SquareHorizontalCharacter.pairing line 187
  18. lemma OAI.SquareHorizontalCharacter.lower_commutator line 190
  19. lemma OAI.SquareHorizontalCharacter.pairing_mul_right line 200
  20. lemma OAI.SquareHorizontalCharacter.pairing_mul_left line 211
  21. def OAI.SquareHorizontalCharacter.pairingHom line 223
  22. lemma OAI.SquareHorizontalCharacter.pairing_self line 233
  23. lemma OAI.SquareHorizontalCharacter.pairing_swap line 240
  24. lemma OAI.SquareHorizontalCharacter.diagonal_conj line 248
  25. lemma OAI.SquareHorizontalCharacter.conjugate_lower line 255
  26. lemma OAI.SquareHorizontalCharacter.conjugate_diagonal line 265
  27. theorem OAI.SquareHorizontalCharacter.conjugate_character line 282
  28. theorem OAI.SquareHorizontalCharacter.character_lattice_iff line 293
  29. lemma OAI.SquareHorizontalCharacter.pairing_lattice line 309
  30. lemma OAI.SquareHorizontalCharacter.continuous_diagonal line 320
  31. lemma OAI.SquareHorizontalCharacter.continuous_lower line 325
  32. lemma OAI.SquareHorizontalCharacter.continuous_pairing line 330