OAI/RingTheory/Multiplicity/LechHilbertSerre.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Lech.hilbertSerre line 32
2. lemma OAI.Lech.IdealGraded.eventuallyPolynomial_piece line 129
3. lemma OAI.Lech.IdealGraded.eventuallyPolynomial_length line 140
4. lemma OAI.Lech.degree_le_of_nat_bound line 162
5. lemma OAI.Lech.exists_polynomial_div_limit line 182
6. lemma OAI.Lech.exists_div_limit_of_eventually_polynomial line 196
7. theorem OAI.Lech.multiplicity_is_limit line 222
8. lemma OAI.Lech.LengthHilbert.eventually_eq_bot line 246
9. lemma OAI.Lech.LengthHilbert.subPiece_length line 269
10. lemma OAI.Lech.LengthHilbert.pieceMap_surjective line 282
11. lemma OAI.Lech.LengthHilbert.pieceMap_ker line 288
12. lemma OAI.Lech.LengthHilbert.length_range_add_length_ker line 293
13. lemma OAI.Lech.LengthHilbert.length_recurrence line 302
14. lemma OAI.Lech.LengthHilbert.quotient_generators line 330
15. lemma OAI.Lech.LengthHilbert.finite_of_no_generators line 344
16. lemma OAI.Lech.LengthHilbert.ker_smul_killed line 353
17. lemma OAI.Lech.LengthHilbert.coker_smul_killed line 358
18. theorem OAI.Lech.LengthHilbert.hilbertSerre line 371