OAI/Analysis/Pureness/Divisibility/HereditarySplitting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.hereditary_complex_smul_mem line 11
2. lemma OAI.CuntzPureness.hereditary_realPart_mem line 21
3. lemma OAI.CuntzPureness.hereditary_imaginaryPart_mem line 27
4. lemma OAI.CuntzPureness.trace_selfAdjoint_im_zero line 34
5. lemma OAI.CuntzPureness.trace_zero_selfadjoint_split line 43
6. theorem OAI.CuntzPureness.exists_orthogonal_pair_hereditary line 70