OAI/Probability/InvariantIsing/Haar/ReflectionParity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Even nonzero reflection factorizations of special orthogonal matrices.

  1. lemma OAI.InvariantIsing.rotationMatrix_list_prod line 12
  2. lemma OAI.InvariantIsing.reflectionList_remove_zero line 18
  3. lemma OAI.InvariantIsing.reflectionList_det line 29
  4. lemma OAI.InvariantIsing.specialRotation_even_reflections line 41