OAI/NumberTheory/PiExponent/Approximation/LinePowerLaws.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponent.NumericalAmpleness.isIso_of_locally_isIso line 11
  2. lemma OAI.PiExponentSeshadri.TensorLocalization.map_tensor_right_unit line 31
  3. lemma OAI.PiExponentSeshadri.Geometry.sheafification_tensor_right_isIso line 56
  4. lemma OAI.PiExponentSeshadri.Geometry.sheafification_tensor_left_isIso line 112
  5. def OAI.PiExponentSeshadri.Geometry.sheafificationTensorRight line 133
  6. def OAI.PiExponentSeshadri.Geometry.sheafificationTensorLeft line 149
  7. def OAI.PiExponentSeshadri.Geometry.lineTensorAssoc line 165
  8. def OAI.PiExponentSeshadri.Geometry.linePowerAdd line 175
  9. def OAI.PiExponentSeshadri.Geometry.linePowerMul line 185