OAI/Analysis/Kaplansky/Ultrapower/Quotient.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.QuasiValue.q_eq_of_null_sub line 15
2. def OAI.KaplanskyConsequences.QuasiValue.quotQ line 23
3. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_map line 26
4. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_nonneg line 28
5. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_zero line 32
6. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_one line 33
7. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_star line 35
8. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_eq_zero line 39
9. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_bound line 43
10. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_projection_lift line 57
11. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_partial_projection line 65
12. lemma OAI.KaplanskyConsequences.QuasiValue.projection_add line 74
13. lemma OAI.KaplanskyConsequences.QuasiValue.selfAdjoint_lift line 81
14. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_projection_add line 94