OAI/Algebra/FinitisticAsymmetry/Rickard/NonGeneration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.Rickard.prop_injective_of_da line 21
2. lemma OAI.LittleFinitistic.Rickard.not_generate_of_minimal_family line 72
3. lemma OAI.LittleFinitistic.Rickard.not_injectivesGenerate_of_little_eq_top line 119