OAI/AlgebraicGeometry/Seshadri/Sheaves/TensorDivision.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Geometry.frameOnSmaller line 20
  2. lemma OAI.MaximalSeshadri.Geometry.common_affine_frames line 26
  3. def OAI.MaximalSeshadri.Geometry.LineBundle.tensor line 38
  4. lemma OAI.MaximalSeshadri.Geometry.sectionMultiply_eq line 45
  5. def OAI.MaximalSeshadri.Geometry.tensorFrame line 61
  6. def OAI.MaximalSeshadri.Geometry.tensorUnitTwist line 68
  7. lemma OAI.MaximalSeshadri.Geometry.tensor_multiply_framed line 74
  8. lemma OAI.MaximalSeshadri.Geometry.tensor_multiply_ideal line 134
  9. theorem OAI.MaximalSeshadri.Geometry.divide_by_generated_section line 147
  10. theorem OAI.MaximalSeshadri.Geometry.divide_by_power_section line 164
  11. lemma OAI.MaximalSeshadri.Geometry.global_quotient_ne_zero line 195