OAI/Analysis/Kaplansky/Quotient/QuotientStable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyConsequences.matrixMap line 16
2. lemma OAI.KaplanskyConsequences.matrixMap_apply line 32
3. lemma OAI.KaplanskyConsequences.matrixMap_surjective line 35
4. abbrev OAI.KaplanskyConsequences.SpectralKernel.FaithfulQuotient line 44
5. def OAI.KaplanskyConsequences.SpectralKernel.quotientHom line 46
6. lemma OAI.KaplanskyConsequences.SpectralKernel.quotientHom_surjective line 49
7. lemma OAI.KaplanskyConsequences.SpectralKernel.quotientHom_eq_zero line 52
8. instance OAI.KaplanskyConsequences.SpectralKernel.faithfulQuotient_nontrivial line 57
9. lemma OAI.KaplanskyConsequences.SpectralKernel.matrixMap_quotient_eq_zero line 65
10. theorem OAI.KaplanskyConsequences.SpectralKernel.faithfulQuotient_stablyFinite line 77