OAI/RingTheory/Multiplicity/FieldNilpotentLift.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.FieldLift.pow_eq_of_quotient_eq line 14
2. def OAI.Lech.FieldLift.liftElement line 22
3. lemma OAI.Lech.FieldLift.liftElement_spec line 24
4. def OAI.Lech.FieldLift.powLift line 28
5. lemma OAI.Lech.FieldLift.powLift_eq line 48
6. lemma OAI.Lech.FieldLift.powLift_mod line 53
7. structure OAI.Lech.FieldPartialLift.Lifts line 62
8. instance OAI.Lech.FieldPartialLift.Lifts.(instance at line 67) line 67
9. instance OAI.Lech.FieldPartialLift.Lifts.(instance at line 79) line 79
10. def OAI.Lech.FieldPartialLift.Lifts.union line 87
11. lemma OAI.Lech.FieldPartialLift.Lifts.le_union line 99
12. lemma OAI.Lech.FieldPartialLift.extend_root line 124
13. lemma OAI.Lech.FieldPartialLift.bot_compatible line 183
14. lemma OAI.Lech.FieldPartialLift.mem_union line 191
15. lemma OAI.Lech.FieldPartialLift.compatible_of_mem line 202
16. lemma OAI.Lech.FieldPartialLift.union_compatible line 210
17. lemma OAI.Lech.FieldPartialLift.exists_lift_of_roots line 225
18. theorem OAI.Lech.FieldLift.exists_lift line 252
19. theorem OAI.Lech.FieldLift.exists_lift_surjective line 276