OAI/Analysis/JiangSu/Nonunital/Essentiality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalSI.left_identity_isStarProjection line 18
2. lemma OAI.NonunitalSI.unitization_action_faithful line 25
3. lemma OAI.NonunitalSI.unitization_representation_injective line 45
4. lemma OAI.NonunitalSI.traceTwoNorm_relative_factorization line 90
5. lemma OAI.NonunitalSI.ideal_factorization_through_unitization line 142