OAI/AlgebraicGeometry/Seshadri/Sheaves/TensorPure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaximalSeshadri.TensorPure.presheaf line 22
2. abbrev OAI.MaximalSeshadri.TensorPure.adj line 25
3. def OAI.MaximalSeshadri.TensorPure.pure line 28
4. lemma OAI.MaximalSeshadri.TensorPure.pure_add_left line 32
5. lemma OAI.MaximalSeshadri.TensorPure.pure_add_right line 38
6. lemma OAI.MaximalSeshadri.TensorPure.pure_smul_left line 44
7. lemma OAI.MaximalSeshadri.TensorPure.pure_smul_right line 51
8. lemma OAI.MaximalSeshadri.TensorPure.pure_restrict line 58
9. lemma OAI.MaximalSeshadri.TensorPure.map_pure line 65
10. lemma OAI.MaximalSeshadri.TensorPure.hom_ext line 73