OAI/Analysis/JiangSu/CStarAlgebras/AmbientIdealConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalIntertwining.ambient_conjugate_mem line 19
2. def OAI.NonunitalIntertwining.ambientConj line 25
3. lemma OAI.NonunitalIntertwining.ambientConj_spec line 28
4. lemma OAI.NonunitalIntertwining.ambientConj_aut_spec line 32
5. def OAI.NonunitalIntertwining.ambientConjHom line 36
6. lemma OAI.NonunitalIntertwining.ambientConj_inv line 45
7. def OAI.NonunitalIntertwining.ambientConjAut line 55
8. lemma OAI.NonunitalIntertwining.ambientConjAut_apply line 61