OAI/RingTheory/Multiplicity/FibreSquare.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.TensorIdeal.idealQuotientMap line 17
2. lemma OAI.Lech.TensorIdeal.idealQuotientMap_mk line 23
3. lemma OAI.Lech.TensorIdeal.quotientTensorEquiv_mk line 26
4. def OAI.Lech.TensorIdeal.kernelSquareEquiv line 40
5. abbrev OAI.Lech.TensorIdeal.unitMap line 66
6. def OAI.Lech.TensorIdeal.fibreMap line 68
7. lemma OAI.Lech.TensorIdeal.fibre_square line 73
8. lemma OAI.Lech.TensorIdeal.fibreMap_surjective line 84
9. def OAI.Lech.TensorIdeal.fibreKernelEquiv line 92
10. lemma OAI.Lech.TensorIdeal.fibreMap_kernel_zero line 99