OAI/NumberTheory/PiExponent/Approximation/ModuleLinePowerLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.lineTensorPresheafRestrictFrame line 13
  2. lemma OAI.PiExponentSeshadri.Geometry.lineTensorPresheaf_unit_restrict_isIso line 26
  3. lemma OAI.PiExponentSeshadri.Geometry.sheafification_tensor_left_line_unit_isIso line 49
  4. def OAI.PiExponentSeshadri.Geometry.sheafificationTensorLeftLinePair line 96
  5. def OAI.PiExponentSeshadri.Geometry.moduleLineTensorAssoc line 109
  6. def OAI.PiExponentSeshadri.Geometry.moduleTwistPowerIso line 119
  7. def OAI.PiExponentSeshadri.Geometry.moduleTwistPowerMulIso line 126