OAI/Analysis/JiangSu/TensorProducts/SimpleCStarAlgebraic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Pureness.topologicallySimple_isSimpleRing line 12
2. theorem OAI.Pureness.simple_complex_center_scalar line 32
3. lemma OAI.Pureness.commuting_relation_finiteIdealSum line 63
4. lemma OAI.Pureness.exists_finiteIdealSum_one line 81
5. theorem OAI.Pureness.commuting_relation_coefficients_zero line 90
6. theorem OAI.Pureness.commutingAlgTensorHom_injective line 153