OAI/Analysis/JiangSu/Excision/PureGNSCommutant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PureStateExcision.sqrt_apply_sqrt line 19
2. lemma OAI.PureStateExcision.sqrt_vector_value line 24
3. lemma OAI.PureStateExcision.sqrt_vector_sum line 38
4. lemma OAI.PureStateExcision.vector_eq_of_cyclic_values line 50
5. theorem OAI.PureStateExcision.pure_gns_positive_commutant line 66
6. lemma OAI.PureStateExcision.selfadjoint_affine_effect line 132
7. lemma OAI.PureStateExcision.pure_gns_selfadjoint_commutant line 158
8. theorem OAI.PureStateExcision.pure_gns_scalar_commutant line 179