OAI/Analysis/Commutator/L2InfiniteSumCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Decomposable.infiniteSumEquiv_single line 26
2. lemma OAI.Kadison.Decomposable.evalL_infiniteSumEquiv line 31
3. def OAI.Kadison.Decomposable.scalarVectorMultiplier line 42
4. lemma OAI.Kadison.Decomposable.scalarVectorMultiplier_ae line 51
5. lemma OAI.Kadison.Decomposable.evalL_scalarMultiplier line 55
6. lemma OAI.Kadison.Decomposable.infiniteSumEquiv_scalar line 68