OAI/AlgebraicGeometry/Seshadri/Divisors/MixedSections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Geometry.mixedPowMap line 17
  2. lemma OAI.MaximalSeshadri.Geometry.mixedPowMap_const line 22
  3. lemma OAI.MaximalSeshadri.Geometry.mixedPowMap_comp line 31
  4. lemma OAI.MaximalSeshadri.Geometry.mixedPowMap_restrict line 42
  5. def OAI.MaximalSeshadri.Geometry.mixedEnd line 69
  6. lemma OAI.MaximalSeshadri.Geometry.mixedEnd_value line 73
  7. lemma OAI.MaximalSeshadri.Geometry.mixedPowMap_unitPower line 82
  8. def OAI.MaximalSeshadri.Geometry.mixedPowerSection line 110
  9. lemma OAI.MaximalSeshadri.Geometry.mixedPowerSection_const line 113
  10. lemma OAI.MaximalSeshadri.Geometry.mixedPowerSection_coefficient line 117
  11. lemma OAI.MaximalSeshadri.Geometry.restrictMixedPowerSection_factor line 130
  12. lemma OAI.MaximalSeshadri.Geometry.local_mixedPowerSection_coefficient line 152