OAI/Probability/InvariantIsing/Gaussian/HermitianQuadraticCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real quadratic form in its actual orthonormal eigenvector coordinates.

  1. lemma OAI.InvariantIsing.hermitian_quadratic_coordinates line 11