OAI/Analysis/Kaplansky/Quotient/MatrixKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyConsequences.SpectralKernel.single line 17
2. def OAI.KaplanskyConsequences.SpectralKernel.oneByOne line 20
3. lemma OAI.KaplanskyConsequences.SpectralKernel.oneByOne_apply line 22
4. lemma OAI.KaplanskyConsequences.SpectralKernel.single_apply line 24
5. lemma OAI.KaplanskyConsequences.SpectralKernel.single_star line 27
6. lemma OAI.KaplanskyConsequences.SpectralKernel.single_mul line 33
7. lemma OAI.KaplanskyConsequences.SpectralKernel.single_compress line 39
8. lemma OAI.KaplanskyConsequences.SpectralKernel.null_single_iff line 45
9. lemma OAI.KaplanskyConsequences.SpectralKernel.null_iff_entries line 67