OAI/NumberTheory/PiExponent/Approximation/FrameTensorPowers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Geometry.tensor_unit_end line 12
  2. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorUnit_scalar line 18
  3. def OAI.PiExponentSeshadri.Geometry.endPower line 43
  4. lemma OAI.PiExponentSeshadri.Geometry.endValue_endPower line 47
  5. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorUnit_natural line 60
  6. lemma OAI.PiExponentSeshadri.Geometry.modulePowMap_unitPower line 88
  7. def OAI.PiExponentSeshadri.Geometry.globalPowerFrame line 116
  8. lemma OAI.PiExponentSeshadri.Geometry.powerSection_coefficient line 120
  9. lemma OAI.PiExponentSeshadri.Geometry.frameChange_globalPowerFrame line 129