OAI/Analysis/Kaplansky/Ultrapower/QuasiFinite.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.QuasiValue.finite_mod_null line 14
2. abbrev OAI.KaplanskyConsequences.QuasiValue.FaithfulQuotient line 68
3. abbrev OAI.KaplanskyConsequences.QuasiValue.quotientHom line 69
4. lemma OAI.KaplanskyConsequences.QuasiValue.faithfulQuotient_nontrivial line 71
5. lemma OAI.KaplanskyConsequences.QuasiValue.faithfulQuotient_finite line 78