OAI/Analysis/MatrixSigning/Matrices/RealDecode.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.HermitianCoordinates.realDecode line 13
  2. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_inl_inl line 19
  3. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_inl_inr line 23
  4. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_inr_inl line 28
  5. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_inr_inr line 33
  6. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_isSymm line 37
  7. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_eq_realify line 59
  8. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_map line 64
  9. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_add line 72
  10. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_smul line 77
  11. def OAI.CurrentKS.HermitianCoordinates.realDecodeLinear line 82
  12. lemma OAI.CurrentKS.HermitianCoordinates.realDecode_ratCast line 88