OAI/RingTheory/Multiplicity/RootUlrichSpan.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.UniversalSplitting.degree_fill line 14
2. lemma OAI.Lech.UniversalSplitting.power_in_homogeneous_span line 35
3. def OAI.Lech.UniversalSplitting.binaryPower line 44
4. lemma OAI.Lech.UniversalSplitting.powerMonomial_mem_binary_span line 49
5. lemma OAI.Lech.UniversalSplitting.Data.binaryPower_span_eq_top line 68
6. instance OAI.Lech.UniversalSplitting.powerIndexFintype line 78
7. theorem OAI.Lech.UniversalSplitting.Data.exists_binary_basis line 87
8. def OAI.Lech.UniversalSplitting.powerWeight line 105
9. def OAI.Lech.UniversalSplitting.powerExponent line 107
10. lemma OAI.Lech.UniversalSplitting.powerWeight_succ line 111
11. lemma OAI.Lech.UniversalSplitting.powerExponent_bound line 114
12. lemma OAI.Lech.UniversalSplitting.binaryPower_prod line 127