OAI/LinearAlgebra/CirculantHadamard/CyclicRing.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

The finite cyclic group ring, with coefficient conjugation and index reversal.

  1. abbrev OAI.CirculantHadamard.CyclicRing.Elem line 18
  2. def OAI.CirculantHadamard.CyclicRing.groupStar line 20
  3. theorem OAI.CirculantHadamard.CyclicRing.groupStar_apply line 24
  4. theorem OAI.CirculantHadamard.CyclicRing.groupStar_groupStar line 28
  5. theorem OAI.CirculantHadamard.CyclicRing.groupStar_single line 34
  6. def OAI.CirculantHadamard.CyclicRing.ofCoeffs line 49
  7. theorem OAI.CirculantHadamard.CyclicRing.ofCoeffs_apply line 53
  8. theorem OAI.CirculantHadamard.CyclicRing.ofCoeffs_coeffs line 56
  9. def OAI.CirculantHadamard.CyclicRing.scalar line 60
  10. theorem OAI.CirculantHadamard.CyclicRing.scalar_apply line 63
  11. theorem OAI.CirculantHadamard.CyclicRing.scalar_natCast line 68
  12. def OAI.CirculantHadamard.CyclicRing.ringStar line 71
  13. theorem OAI.CirculantHadamard.CyclicRing.ringStar_apply line 75
  14. theorem OAI.CirculantHadamard.CyclicRing.ringStar_eq_groupStar line 79
  15. theorem OAI.CirculantHadamard.CyclicRing.ringStar_single line 82
  16. theorem OAI.CirculantHadamard.CyclicRing.group_mul_apply line 91
  17. theorem OAI.CirculantHadamard.CyclicRing.group_mul_apply_right line 100
  18. theorem OAI.CirculantHadamard.CyclicRing.groupStar_zero line 108
  19. theorem OAI.CirculantHadamard.CyclicRing.groupStar_add line 113
  20. theorem OAI.CirculantHadamard.CyclicRing.groupStar_one line 119
  21. theorem OAI.CirculantHadamard.CyclicRing.groupStar_mul line 125
  22. theorem OAI.CirculantHadamard.CyclicRing.mul_apply line 138
  23. theorem OAI.CirculantHadamard.CyclicRing.mul_apply_right line 142
  24. theorem OAI.CirculantHadamard.CyclicRing.ringStar_ringStar line 146
  25. theorem OAI.CirculantHadamard.CyclicRing.ringStar_zero line 150
  26. theorem OAI.CirculantHadamard.CyclicRing.ringStar_add line 153
  27. theorem OAI.CirculantHadamard.CyclicRing.ringStar_one line 157
  28. theorem OAI.CirculantHadamard.CyclicRing.ringStar_mul line 160
  29. theorem OAI.CirculantHadamard.CyclicRing.ringStar_scalar line 164
  30. theorem OAI.CirculantHadamard.CyclicRing.mul_ringStar_apply line 170
  31. def OAI.CirculantHadamard.CyclicRing.groupStarRingHom line 175
  32. def OAI.CirculantHadamard.CyclicRing.ringStarRingHom line 183
  33. theorem OAI.CirculantHadamard.CyclicRing.ringStarRingHom_apply line 186
  34. def OAI.CirculantHadamard.CyclicRing.augmentation line 189
  35. theorem OAI.CirculantHadamard.CyclicRing.augmentation_apply line 192
  36. theorem OAI.CirculantHadamard.CyclicRing.augmentation_scalar line 198
  37. theorem OAI.CirculantHadamard.CyclicRing.augmentation_ringStar line 204
  38. theorem OAI.CirculantHadamard.CyclicRing.augmentation_norm_star line 210
  39. theorem OAI.CirculantHadamard.CyclicRing.augmentation_norm line 217