OAI/RingTheory/Multiplicity/ReesRootPowerPath.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.IdealFiltered.rowMap_power_range line 15
2. abbrev OAI.Lech.ReesRoot.enlargedPath line 31
3. lemma OAI.Lech.ReesRoot.enlarged_power_range line 36
4. lemma OAI.Lech.ReesRoot.enlarged_power_injective line 42
5. lemma OAI.Lech.ReesRoot.enlargedStep_range line 47
6. lemma OAI.Lech.ReesRoot.enlargedPath_range line 53
7. lemma OAI.Lech.ReesRoot.enlargedPath_injective line 61
8. theorem OAI.Lech.ReesRoot.uniform_unit_nilpotence line 71