OAI/RingTheory/Multiplicity/PowerSeriesFlatVariables.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.PowerSeries.flat_variables_weaklyRegular line 25
2. lemma OAI.Lech.PowerSeries.perfect_free_variables_weaklyRegular line 32
3. lemma OAI.Lech.weaklyRegular_map_of_flat line 50
4. lemma OAI.Lech.PowerSeries.variables_pow_weaklyRegular line 64
5. lemma OAI.Lech.PowerSeries.perfect_free_variables_pow_weaklyRegular line 73
6. instance OAI.Lech.Koszul.(instance at line 97) line 97
7. instance OAI.Lech.Koszul.(instance at line 108) line 108
8. lemma OAI.Lech.Koszul.cone_homology_zero_of_mono line 197
9. def OAI.Lech.Koszul.singleModule line 244
10. def OAI.Lech.Koszul.singleTensorHomologyZeroIso line 247
11. lemma OAI.Lech.Koszul.tensor_single_homology_zero_of_regular line 259