OAI/CategoryTheory/ThickClosure/PrincipalModules.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HahnWilson.PrincipalModules.IsTorsionModule line 13
2. lemma OAI.HahnWilson.PrincipalModules.ideal_free line 19
3. def OAI.HahnWilson.PrincipalModules.splitEquiv line 40
4. theorem OAI.HahnWilson.PrincipalModules.finite_free_submodule line 59
5. lemma OAI.HahnWilson.PrincipalModules.common_left_multiple line 97
6. def OAI.HahnWilson.PrincipalModules.principalOreSet line 126
7. theorem OAI.HahnWilson.PrincipalModules.finite_free_resolution line 136
8. abbrev OAI.HahnWilson.PrincipalModules.FractionRing line 169
9. def OAI.HahnWilson.PrincipalModules.moduleNumerator line 174
10. lemma OAI.HahnWilson.PrincipalModules.numerator_eq_zero_iff line 179
11. lemma OAI.HahnWilson.PrincipalModules.localization_finite line 190
12. lemma OAI.HahnWilson.PrincipalModules.common_right_multiple line 220
13. lemma OAI.HahnWilson.PrincipalModules.right_denominator line 227
14. lemma OAI.HahnWilson.PrincipalModules.common_right_denominator line 240
15. lemma OAI.HahnWilson.PrincipalModules.integral_coordinate line 259
16. lemma OAI.HahnWilson.PrincipalModules.torsion_kernel_map line 297
17. theorem OAI.HahnWilson.PrincipalModules.torsion_free_decomposition line 329