OAI/Analysis/Commutator/RationalDense.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.RationalDense.subspace line 22
2. instance OAI.Kadison.RationalDense.(instance at line 24) line 24
3. lemma OAI.Kadison.RationalDense.dense line 26
4. lemma OAI.Kadison.RationalDense.exists_seq line 30
5. def OAI.Kadison.ComplexLinearization.part line 42
6. lemma OAI.Kadison.ComplexLinearization.part_apply line 45
7. lemma OAI.Kadison.ComplexLinearization.part_map_I line 48
8. lemma OAI.Kadison.ComplexLinearization.complex_smul line 54
9. def OAI.Kadison.ComplexLinearization.operator line 62
10. lemma OAI.Kadison.ComplexLinearization.operator_apply line 68
11. lemma OAI.Kadison.ComplexLinearization.norm_le line 71