OAI/Analysis/FreeWords/PartialUnitaryAlgebra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KKLocalPatching.PartialUnitary line 9
  2. def OAI.KKLocalPatching.PartialUnitary.support line 18
  3. theorem OAI.KKLocalPatching.PartialUnitary.support_mul line 20
  4. theorem OAI.KKLocalPatching.PartialUnitary.mul_support line 23
  5. theorem OAI.KKLocalPatching.PartialUnitary.projection line 26
  6. theorem OAI.KKLocalPatching.PartialUnitary.star_power_mul line 32
  7. theorem OAI.KKLocalPatching.PartialUnitary.power_mul_star line 36
  8. def OAI.KKLocalPatching.PartialUnitary.zero line 40
  9. theorem OAI.KKLocalPatching.PartialUnitary.orthogonal_power line 45
  10. theorem OAI.KKLocalPatching.PartialUnitary.orthogonal_symm line 52
  11. def OAI.KKLocalPatching.PartialUnitary.sum line 58
  12. theorem OAI.KKLocalPatching.PartialUnitary.sum_power line 65
  13. theorem OAI.KKLocalPatching.PartialUnitary.sum_support line 68
  14. def OAI.KKLocalPatching.PartialUnitary.toUnitary line 71
  15. theorem OAI.KKLocalPatching.PartialUnitary.toUnitary_power line 74