OAI/RingTheory/Multiplicity/SeparableOrderNormalizedLength.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Lech.SeparableOrder.normalizedLength_coordinate_power_koszul line 47
2. theorem OAI.Lech.SeparableOrder.normalizedLength_parameter_koszul line 95
3. def OAI.Lech.Grading.projection line 185
4. lemma OAI.Lech.Grading.projection_apply line 189
5. lemma OAI.Lech.Grading.proj_of_mem line 192
6. lemma OAI.Lech.Grading.projection_succ_comp line 203
7. lemma OAI.Lech.Grading.projection_zero_comp line 214
8. lemma OAI.Lech.Grading.ker_homogeneous line 224
9. lemma OAI.Lech.Grading.range_homogeneous line 230
10. def OAI.Lech.Grading.step line 243
11. lemma OAI.Lech.Grading.step_apply line 248
12. lemma OAI.Lech.Grading.step_ker line 252
13. lemma OAI.Lech.Grading.step_range line 256
14. lemma OAI.Lech.Grading.eventually_eq_bot line 279
15. lemma OAI.Lech.Grading.subPiece_finrank line 302
16. lemma OAI.Lech.Grading.pieceMap_surjective line 315
17. lemma OAI.Lech.Grading.pieceMap_ker line 321
18. lemma OAI.Lech.Grading.finrank_recurrence line 326
19. def OAI.Lech.sumPolynomial line 349
20. lemma OAI.Lech.sumPolynomial_eval line 353
21. def OAI.Lech.EventuallyPolynomial line 368
22. lemma OAI.Lech.eventuallyPolynomial_zero line 371
23. lemma OAI.Lech.EventuallyPolynomial.add line 374
24. lemma OAI.Lech.EventuallyPolynomial.sub line 381
25. lemma OAI.Lech.EventuallyPolynomial.succ line 388
26. lemma OAI.Lech.EventuallyPolynomial.of_sub_succ line 396
27. lemma OAI.Lech.EventuallyPolynomial.of_recurrence line 419
28. lemma OAI.Lech.quotient_generators line 437
29. lemma OAI.Lech.finite_of_no_generators line 451
30. lemma OAI.Lech.ker_smul_killed line 460
31. lemma OAI.Lech.coker_smul_killed line 465