OAI/Analysis/Commutator/CoefficientForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.PreHilbert.wordSpace line 16
2. def OAI.Kadison.PreHilbert.word line 18
3. lemma OAI.Kadison.PreHilbert.norm_word line 21
4. lemma OAI.Kadison.PreHilbert.inner_word line 25
5. lemma OAI.Kadison.PreHilbert.word_add_left line 30
6. lemma OAI.Kadison.PreHilbert.word_smul_left line 34
7. lemma OAI.Kadison.PreHilbert.word_update_add line 38
8. lemma OAI.Kadison.PreHilbert.word_update_smul line 44