OAI/Probability/InvariantIsing/Haar/RotationMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Matrix coordinates for Euclidean isometries and hyperplane reflections.

  1. def OAI.InvariantIsing.rotationMatrix line 12
  2. lemma OAI.InvariantIsing.rotationMatrix_apply line 16
  3. lemma OAI.InvariantIsing.rotationMatrix_mem line 22
  4. lemma OAI.InvariantIsing.rotationMatrix_mul line 27
  5. lemma OAI.InvariantIsing.rotationMatrix_one line 31
  6. lemma OAI.InvariantIsing.rotationMatrix_specialRotation line 34
  7. def OAI.InvariantIsing.hyperplaneReflection line 41
  8. lemma OAI.InvariantIsing.hyperplaneReflection_zero line 44
  9. lemma OAI.InvariantIsing.hyperplaneReflection_apply line 51
  10. lemma OAI.InvariantIsing.rotationMatrix_reflection_apply line 57
  11. lemma OAI.InvariantIsing.rotationMatrix_reflection_det line 68