OAI/Algebra/FinitisticAsymmetry/Kasch/ProjectiveSplitting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.Kasch.annihilates_radical line 23
2. lemma OAI.LittleFinitistic.Kasch.finsupp_mem_radical_of_annihilated line 34
3. lemma OAI.LittleFinitistic.Kasch.projective_mem_radical_iff line 50
4. lemma OAI.LittleFinitistic.Kasch.projective_mono_reflects_radical line 66
5. lemma OAI.LittleFinitistic.Kasch.projective_mono_splits line 79