OAI/Analysis/IrrationalRotation/Rotation/DiagonalAdjoint.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantRotation.DiagonalAdjoint.Hilbert line 14
2. theorem OAI.InvariantRotation.DiagonalAdjoint.isFormalAdjoint_diagonal line 16
3. theorem OAI.InvariantRotation.DiagonalAdjoint.adjoint_apply_coordinate line 31
4. theorem OAI.InvariantRotation.DiagonalAdjoint.adjoint_eq_diagonal line 52
5. theorem OAI.InvariantRotation.DiagonalAdjoint.isSelfAdjoint_of_real_diagonal line 79
6. theorem OAI.InvariantRotation.DiagonalAdjoint.quadraticForm_nonneg line 94