OAI/Probability/SignedSweeps/UnitaryTensorSpan.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.cayley_real_denom_ne line 10
  2. lemma OAI.SignedSweeps.cayley_real_norm line 15
  3. lemma OAI.SignedSweeps.cayley_real_injective line 23
  4. lemma OAI.SignedSweeps.infinite_complex_unit_sphere line 33
  5. lemma OAI.SignedSweeps.span_unit_monomial_evaluations line 38
  6. def OAI.SignedSweeps.wordTensorMatrixHom line 65
  7. def OAI.SignedSweeps.unitaryTensorAlgebra line 71
  8. lemma OAI.SignedSweeps.unitaryTensorAlgebra_toSubmodule line 75
  9. lemma OAI.SignedSweeps.wordUnitary_mem line 84
  10. lemma OAI.SignedSweeps.diagonal_unitary line 88
  11. theorem OAI.SignedSweeps.diagonal_wordTensor_mem line 100
  12. lemma OAI.SignedSweeps.hermitian_wordTensor_mem line 141
  13. theorem OAI.SignedSweeps.wordTensor_mem_unitary line 151
  14. theorem OAI.SignedSweeps.span_unitary_wordTensor line 171