OAI/RingTheory/Multiplicity/RootTowerNormalizedLength.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Lech.RootTower.normalizedLength_root_quotient line 27
2. lemma OAI.Lech.RootTower.perfectMap_surjective line 39
3. def OAI.Lech.RootTower.perfectAlgHom line 61
4. def OAI.Lech.RootTower.perfectAlgEquiv line 70
5. lemma OAI.Lech.RootTower.perfectAlgEquiv_of line 76
6. theorem OAI.Lech.FrobeniusIntermediate.normalizedLength_intermediate_quotient line 95
7. theorem OAI.Lech.SeparableOrder.exists_normalization_frobenius_limit line 152
8. lemma OAI.Lech.NormalizedLength.Tower.length_fin line 227
9. lemma OAI.Lech.NormalizedLength.Tower.exists_length_le_mul_quotient line 235
10. theorem OAI.Lech.NormalizedLength.Tower.length_eq_zero_of_small_annihilators line 260
11. lemma OAI.Lech.RootTower.normalizedLength_base_root_quotient line 286
12. lemma OAI.Lech.RootTower.frobenius_root_ideal line 302
13. lemma OAI.Lech.RootTower.root_scalar_quotient_tendsto line 316
14. lemma OAI.Lech.RootTower.normalizedLength_eq_zero_of_root_annihilated line 338
15. lemma OAI.Lech.baseChange_scalar_factorization line 367
16. theorem OAI.Lech.PerfectDomainStages.exists_root_finite_free_factorization line 387
17. lemma OAI.Lech.PowerSeries.killSucc_surjective line 428
18. lemma OAI.Lech.PowerSeries.killSucc_ker line 433
19. lemma OAI.Lech.PowerSeries.variables_weaklyRegular line 457