OAI/RingTheory/Multiplicity/ScalarCartierLift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.TensorIdeal.scalarLift line 14
2. lemma OAI.Lech.TensorIdeal.scalarLift_comp line 21
3. def OAI.Lech.TotalGhost.scalarRowLift line 36
4. lemma OAI.Lech.TotalGhost.scalarRowLift_comp line 44
5. def OAI.Lech.TotalGhost.scalarLift line 51
6. lemma OAI.Lech.TotalGhost.scalarLift_comp line 58
7. lemma OAI.Lech.TotalGhost.total_map_smul line 63
8. lemma OAI.Lech.TotalGhost.annihilator_of_nilpotence line 74