OAI/Algebra/FinitisticAsymmetry/Nakayama/Coinduction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.Nakayama.da_finite line 14
2. def OAI.LittleFinitistic.Nakayama.coindLine line 19
3. lemma OAI.LittleFinitistic.Nakayama.coindLine_apply line 24
4. lemma OAI.LittleFinitistic.Nakayama.coind_zero_eval line 28
5. lemma OAI.LittleFinitistic.Nakayama.coind_sum_eval line 32
6. def OAI.LittleFinitistic.Nakayama.coindBasisMap line 40
7. lemma OAI.LittleFinitistic.Nakayama.coindBasisMap_injective line 46
8. lemma OAI.LittleFinitistic.Nakayama.coindBasisMap_surjective line 77
9. lemma OAI.LittleFinitistic.Nakayama.coindBasisMap_bijective line 114
10. def OAI.LittleFinitistic.Nakayama.moduleCoindInclusion line 118
11. lemma OAI.LittleFinitistic.Nakayama.moduleCoindInclusion_mono line 123