OAI/Algebra/FinitisticAsymmetry/Nakayama/Minimality.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LittleFinitistic.Nakayama.split_of_dual_surjectiveline 14 - lemma
OAI.LittleFinitistic.Nakayama.nakayama_map_not_injectiveline 29 - lemma
OAI.LittleFinitistic.Nakayama.minimal_differential_not_splitline 42 - lemma
OAI.LittleFinitistic.Nakayama.minimal_nakayama_differential_noninjectiveline 71