OAI/Analysis/Kaplansky/Ultrapower/QuasiNull.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.QuasiValue.val_add_of_zero line 14
2. abbrev OAI.KaplanskyConsequences.QuasiValue.IsNull line 29
3. lemma OAI.KaplanskyConsequences.QuasiValue.null_zero line 31
4. lemma OAI.KaplanskyConsequences.QuasiValue.null_star line 33
5. lemma OAI.KaplanskyConsequences.QuasiValue.null_add line 36
6. lemma OAI.KaplanskyConsequences.QuasiValue.null_smul line 51
7. lemma OAI.KaplanskyConsequences.QuasiValue.null_mul_left line 61
8. lemma OAI.KaplanskyConsequences.QuasiValue.null_mul_right line 73
9. lemma OAI.KaplanskyConsequences.QuasiValue.continuous_squareVal line 77
10. def OAI.KaplanskyConsequences.QuasiValue.nullIdeal line 87
11. lemma OAI.KaplanskyConsequences.QuasiValue.val_zero_of_null line 98
12. lemma OAI.KaplanskyConsequences.QuasiValue.null_of_val_zero line 107
13. lemma OAI.KaplanskyConsequences.QuasiValue.null_posPart line 114
14. lemma OAI.KaplanskyConsequences.QuasiValue.null_sub line 118
15. lemma OAI.KaplanskyConsequences.QuasiValue.val_eq_of_null_sub line 121