OAI/GroupTheory/FiniteType/IdempotentEnlargement.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IdempotentEnlargement.RingSpace line 12
  2. abbrev OAI.IdempotentEnlargement.ArraySpace line 13
  3. def OAI.IdempotentEnlargement.permute line 15
  4. lemma OAI.IdempotentEnlargement.permute_single line 26
  5. def OAI.IdempotentEnlargement.coefficients line 30
  6. lemma OAI.IdempotentEnlargement.coefficients_single line 53
  7. lemma OAI.IdempotentEnlargement.coefficients_commute_permute line 57
  8. def OAI.IdempotentEnlargement.groupAlgebraAction line 63
  9. lemma OAI.IdempotentEnlargement.groupAlgebraAction_single line 66
  10. lemma OAI.IdempotentEnlargement.coefficients_commute_groupAlgebra line 71
  11. def OAI.IdempotentEnlargement.representation line 79
  12. lemma OAI.IdempotentEnlargement.representation_tmul_single line 83
  13. def OAI.IdempotentEnlargement.jVal line 90
  14. lemma OAI.IdempotentEnlargement.jVal_eq line 94
  15. lemma OAI.IdempotentEnlargement.jVal_one line 100
  16. lemma OAI.IdempotentEnlargement.jVal_identity line 104
  17. lemma OAI.IdempotentEnlargement.jVal_mul line 108
  18. def OAI.IdempotentEnlargement.unitMap line 119
  19. lemma OAI.IdempotentEnlargement.unitMap_val line 129
  20. lemma OAI.IdempotentEnlargement.jVal_mul_of_orthogonal line 133
  21. lemma OAI.IdempotentEnlargement.unitMap_commute line 141
  22. lemma OAI.IdempotentEnlargement.unitMap_addition line 151
  23. lemma OAI.IdempotentEnlargement.representation_jVal line 159
  24. lemma OAI.IdempotentEnlargement.representation_jVal_fixed line 167
  25. lemma OAI.IdempotentEnlargement.representation_jVal_identity line 172
  26. lemma OAI.IdempotentEnlargement.unitMap_identity_injective line 178
  27. def OAI.IdempotentEnlargement.W line 189
  28. def OAI.IdempotentEnlargement.j line 192
  29. lemma OAI.IdempotentEnlargement.j_val line 196
  30. instance OAI.IdempotentEnlargement.arrayAction line 199
  31. lemma OAI.IdempotentEnlargement.j_smul line 204
  32. lemma OAI.IdempotentEnlargement.j_fixed line 209
  33. lemma OAI.IdempotentEnlargement.j_identity_equivariant line 213
  34. lemma OAI.IdempotentEnlargement.j_identity_injective line 217
  35. lemma OAI.IdempotentEnlargement.j_commute line 222
  36. lemma OAI.IdempotentEnlargement.j_addition line 228
  37. def OAI.IdempotentEnlargement.point line 236
  38. lemma OAI.IdempotentEnlargement.point_injective line 238