OAI/NumberTheory/CubicMoment/Angular/AngularResidueLift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite factor above three compensates the fixed infinity type. It is one on every primary element, so it does not change the original sums.

  1. def OAI.CubicFirstMoment.angularLiftResidueChar line 11
  2. lemma OAI.CubicFirstMoment.angularLiftResidueChar_primary line 15
  3. lemma OAI.CubicFirstMoment.angularLiftResidueChar_compatible line 22
  4. lemma OAI.CubicFirstMoment.productResidueChar_angular_units_right line 29
  5. def OAI.CubicFirstMoment.structuredAngularTwistModulus line 38
  6. def OAI.CubicFirstMoment.structuredAngularTwistCharacter line 41
  7. lemma OAI.CubicFirstMoment.structuredAngularTwistModulus_ne_zero line 46
  8. lemma OAI.CubicFirstMoment.structuredAngularTwistCharacter_compatible line 50
  9. lemma OAI.CubicFirstMoment.structuredAngularTwistModulus_bound line 56