OAI/Analysis/Commutator/PartialUnitaryAlgebra.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Kadison.FinitePatching.PartialUnitary line 17
  2. lemma OAI.Kadison.FinitePatching.PartialUnitary.norm_le_one line 30
  3. lemma OAI.Kadison.FinitePatching.PartialUnitary.star_mul_support line 35
  4. lemma OAI.Kadison.FinitePatching.PartialUnitary.support_mul_star line 39
  5. def OAI.Kadison.FinitePatching.PartialUnitary.power line 43
  6. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_zero line 48
  7. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_nat_succ line 50
  8. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_negSucc line 53
  9. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_support line 56
  10. lemma OAI.Kadison.FinitePatching.PartialUnitary.support_power line 65
  11. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_norm line 73
  12. lemma OAI.Kadison.FinitePatching.PartialUnitary.star_power line 83
  13. lemma OAI.Kadison.FinitePatching.PartialUnitary.orthogonal_support_symm line 91
  14. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_mul_power_zero line 96
  15. lemma OAI.Kadison.FinitePatching.PartialUnitary.val_mul_zero line 102
  16. lemma OAI.Kadison.FinitePatching.PartialUnitary.star_val_mul_zero line 105
  17. lemma OAI.Kadison.FinitePatching.PartialUnitary.val_mul_star_zero line 108
  18. def OAI.Kadison.FinitePatching.PartialUnitary.add line 111
  19. lemma OAI.Kadison.FinitePatching.PartialUnitary.pow_add_of_mul_zero line 142
  20. lemma OAI.Kadison.FinitePatching.PartialUnitary.add_power line 152
  21. def OAI.Kadison.FinitePatching.PartialUnitary.zero line 167
  22. lemma OAI.Kadison.FinitePatching.PartialUnitary.zero_power line 176