OAI/NumberTheory/PiExponent/Approximation/TensorPure.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.TensorPure.presheaf line 19
  2. abbrev OAI.PiExponentSeshadri.TensorPure.adj line 22
  3. def OAI.PiExponentSeshadri.TensorPure.pure line 25
  4. lemma OAI.PiExponentSeshadri.TensorPure.pure_add_left line 29
  5. lemma OAI.PiExponentSeshadri.TensorPure.pure_add_right line 35
  6. lemma OAI.PiExponentSeshadri.TensorPure.pure_smul_left line 41
  7. lemma OAI.PiExponentSeshadri.TensorPure.pure_smul_right line 47
  8. lemma OAI.PiExponentSeshadri.TensorPure.pure_restrict line 53
  9. lemma OAI.PiExponentSeshadri.TensorPure.map_pure line 60
  10. lemma OAI.PiExponentSeshadri.TensorPure.hom_ext line 68
  11. lemma OAI.PiExponentSeshadri.TensorPure.sheafify_restrict_unit line 76
  12. lemma OAI.PiExponentSeshadri.TensorPure.presheaf_restrict_pure line 100
  13. lemma OAI.PiExponentSeshadri.TensorPure.restrict_pure line 108
  14. lemma OAI.PiExponentSeshadri.TensorPure.restrict_pure_inv line 134
  15. lemma OAI.PiExponentSeshadri.TensorPure.restrict_hom_ext line 144
  16. lemma OAI.PiExponentSeshadri.TensorPure.restrict_map line 157
  17. lemma OAI.PiExponentSeshadri.TensorPure.unit_pure line 179
  18. lemma OAI.PiExponentSeshadri.TensorPure.right_unit_pure line 187