OAI/RingTheory/Multiplicity/TowerRestrictedLength.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.NormalizedLength.Tower.restrictedLength_zero_of_ranges line 39
2. lemma OAI.Lech.NormalizedLength.Tower.restrictedLength_directSum_zero line 52
3. lemma OAI.Lech.NormalizedLength.Tower.restrictedLength_directLimit_zero line 66
4. lemma OAI.Lech.NormalizedLength.Tower.restrictedLength_iSup_zero line 81
5. def OAI.Lech.NormalizedLength.Tower.allModuleLength line 123
6. def OAI.Lech.CharP.parameterIdeal line 162
7. theorem OAI.Lech.CharP.exists_length line 167
8. def OAI.Lech.HilbertKunz.normalizedColength line 260
9. def OAI.Lech.HilbertKunz.multiplicity line 264
10. lemma OAI.Lech.CharP.frobeniusIdeal_radical line 279
11. lemma OAI.Lech.CharP.entryIdeal_ofFn line 293
12. lemma OAI.Lech.CharP.quotient_finite_of_parameters line 301
13. lemma OAI.Lech.CharP.hilbertKunz_limit_of_length line 334
14. theorem OAI.Lech.CharP.length_inputs line 358