OAI/Algebra/FinitisticAsymmetry/Derived/ModuleGeneration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.DerivedSupport.prop_single_shortExact₁ line 18
2. lemma OAI.LittleFinitistic.DerivedSupport.prop_single_shortExact₂ line 32
3. lemma OAI.LittleFinitistic.DerivedSupport.prop_single_of_cofan line 46
4. lemma OAI.LittleFinitistic.DerivedSupport.prop_restricted_projective line 61
5. lemma OAI.LittleFinitistic.DerivedSupport.submodule_shortExact line 91
6. lemma OAI.LittleFinitistic.DerivedSupport.prop_annihilated_module line 103
7. lemma OAI.LittleFinitistic.DerivedSupport.prop_of_nilpotent_kernel line 122
8. abbrev OAI.LittleFinitistic.DerivedSupport.coordinateModule line 154
9. lemma OAI.LittleFinitistic.DerivedSupport.prop_restricted_pi line 159
10. lemma OAI.LittleFinitistic.DerivedSupport.prop_all_of_product_augmentation line 180