OAI/RingTheory/Multiplicity/LechFiniteFree.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Lech.finite_free_factorization line 24
2. lemma OAI.Lech.length_kernel_eq_cokernel line 86
3. lemma OAI.Lech.length_torsion_subquotient_le line 103
4. lemma OAI.Lech.length_scalar_cokernel_pi line 138
5. lemma OAI.Lech.length_isogeny line 159
6. lemma OAI.Lech.scalar_range line 209
7. lemma OAI.Lech.scalar_cokernel_quotient_length line 216
8. lemma OAI.Lech.baseChange_isogeny line 228
9. theorem OAI.Lech.finite_module_colength_compare line 253
10. theorem OAI.Lech.finite_module_colength_error line 286
11. lemma OAI.Lech.tendsto_of_abs_sub_le line 330
12. theorem OAI.Lech.finite_module_asymptotic line 342
13. theorem OAI.Lech.finite_module_colength_compare_pos line 367
14. theorem OAI.Lech.finite_module_asymptoticENN line 416