OAI/RingTheory/Multiplicity/TraceConductorPerfectOrder.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.TraceConductor.perfectOrderAt line 22
2. lemma OAI.Lech.TraceConductor.perfectOrderAt_zero line 26
3. lemma OAI.Lech.TraceConductor.perfectOrder_roots line 29
4. lemma OAI.Lech.TraceConductor.root_conductor line 50
5. lemma OAI.Lech.TensorInjection.injective_of_basis line 66
6. lemma OAI.Lech.TensorInjection.field_product_injective line 81
7. lemma OAI.Lech.TensorInjection.localized_product_injective line 97
8. theorem OAI.Lech.TensorInjection.stage_product_injective line 123
9. lemma OAI.Lech.RootTower.rootMap_eq_frobeniusEquiv line 165
10. lemma OAI.Lech.RootTower.rootMap_flat line 174
11. lemma OAI.Lech.RootTower.root_basis_independent line 188
12. lemma OAI.Lech.PerfectStages.stages_mono line 224
13. lemma OAI.Lech.PerfectStages.embedded_perfection_mem line 237
14. lemma OAI.Lech.PerfectStages.embedded_perfection_integral line 247
15. def OAI.Lech.PerfectStages.tensorStageMap line 275
16. lemma OAI.Lech.PerfectStages.tensorStageMap_apply line 291
17. theorem OAI.Lech.PerfectStages.tensorStageMap_injective line 311
18. lemma OAI.Lech.PerfectStages.tensorStageMap_range line 372
19. instance OAI.Lech.PerfectDomainStages.domainAlgebra line 399
20. def OAI.Lech.PerfectDomainStages.stage line 402
21. def OAI.Lech.PerfectDomainStages.tensorMap line 405
22. lemma OAI.Lech.PerfectDomainStages.tensorMap_apply line 415
23. lemma OAI.Lech.PerfectDomainStages.tensorMap_range line 419
24. lemma OAI.Lech.PerfectDomainStages.stage_mono line 438
25. lemma OAI.Lech.PerfectDomainStages.stage_exhaustive line 446
26. def OAI.Lech.PerfectDomainStages.fieldMap line 453
27. lemma OAI.Lech.PerfectDomainStages.fieldMap_tensor line 460
28. lemma OAI.Lech.PerfectDomainStages.tensorMap_injective line 483
29. theorem OAI.Lech.PerfectDomainStages.exists_conductor line 495