OAI/Analysis/MatrixSigning/Matrices/JordanCLMStrictPos.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.Hermitian.jordanCLM_strict_pos line 16