OAI/Analysis/Commutator/FieldAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.Decomposable.FieldMember line 23
2. lemma OAI.Kadison.Decomposable.fieldMember_const line 27
3. lemma OAI.Kadison.Decomposable.fieldMember_zero line 34
4. lemma OAI.Kadison.Decomposable.fieldMember_one line 45
5. lemma OAI.Kadison.Decomposable.fieldMember_add line 55
6. lemma OAI.Kadison.Decomposable.fieldMember_mul line 65
7. lemma OAI.Kadison.Decomposable.fieldMember_smul line 75
8. lemma OAI.Kadison.Decomposable.fieldMember_star line 87
9. def OAI.Kadison.Decomposable.fieldAlgebra line 96