OAI/Probability/InvariantIsing/Haar/HaarPlaneCasimir.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact orthogonal Lie-algebra contractions in the unnormalized Frobenius convention.

  1. lemma OAI.InvariantIsing.sum_planeGenerator_sq line 11
  2. lemma OAI.InvariantIsing.skew_matrix_trace_zero line 19
  3. theorem OAI.InvariantIsing.sum_planeGenerator_double_commutator line 25