OAI/Analysis/KadisonKastler/SignedPermutation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A finite unitary group spanning a full matrix algebra

  1. def OAI.KadisonKastler.permuteSigns line 19

    Source documentation

    Permutations act on diagonal signs by permuting their coordinates.

    def permuteSigns : Equiv.Perm ι →* MulAut (ι → ℤˣ) where
…
  2. abbrev OAI.KadisonKastler.SignedPermutation line 29
  3. instance OAI.KadisonKastler.(instance at line 31) line 31
  4. def OAI.KadisonKastler.signDiagonal line 34
  5. theorem OAI.KadisonKastler.signDiagonal_star line 38
  6. theorem OAI.KadisonKastler.signDiagonal_mul line 45
  7. theorem OAI.KadisonKastler.signDiagonal_sq line 49
  8. def OAI.KadisonKastler.signDiagonalUnitary line 55
  9. def OAI.KadisonKastler.signDiagonalHom line 61
  10. def OAI.KadisonKastler.permutationUnitary line 66
  11. def OAI.KadisonKastler.permutationHom line 76
  12. theorem OAI.KadisonKastler.permutationMatrix_apply line 81
  13. theorem OAI.KadisonKastler.permutation_signDiagonal line 87
  14. def OAI.KadisonKastler.signedPermutationHom line 98

    Source documentation

    The finite signed-permutation group acts by actual unitary matrices.

    def signedPermutationHom : SignedPermutation ι →* unitary (Matrix ι ι ℂ) :=
…

    Mentions: OAI.KadisonKastler.SignedPermutation