OAI/RingTheory/Multiplicity/ReesRootPositivity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ReesRoot.enlargedStep_total_mono line 21
2. lemma OAI.Lech.ReesRoot.enlargedStep_cokernel_property line 27
3. lemma OAI.Lech.ReesRoot.enlargedPath_total_mono line 36
4. lemma OAI.Lech.ReesRoot.enlargedPath_cokernel_property line 52
5. theorem OAI.Lech.ReesRoot.enlargedAtTotal_finite line 81
6. def OAI.Lech.ReesRoot.rootAmbient line 92
7. lemma OAI.Lech.ReesRoot.twistSequence_rootAmbient line 96
8. theorem OAI.Lech.ReesRoot.rootTotal_positive_degree line 104
9. theorem OAI.Lech.ReesRoot.rootTotal_negative_degree line 120