OAI/Analysis/Commutator/FieldAdjoint.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Decomposable.field_inner_integrable line 23
2. lemma OAI.Kadison.Decomposable.field_inner_right_integrable line 34
3. lemma OAI.Kadison.Decomposable.operator_const_inner_indicator line 45
4. lemma OAI.Kadison.Decomposable.const_inner_operator_indicator line 62
5. theorem OAI.Kadison.Decomposable.adjoint_ae line 79