OAI/NumberTheory/CubicMoment/Angular/AngularHeatLattice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact angular ideal/element theta reindexing, including all finite Euler factors and the term at zero.

  1. lemma OAI.CubicFirstMoment.angular_char_unit_mul line 13
  2. lemma OAI.CubicFirstMoment.angular_unitCompatible_dual line 27
  3. lemma OAI.CubicFirstMoment.idealHeatTheta_lattice line 33
  4. def OAI.CubicFirstMoment.angularLatticeHeat line 64
  5. lemma OAI.CubicFirstMoment.theta_at_zero line 69
  6. lemma OAI.CubicFirstMoment.angularLatticeHeat_eq line 73
  7. lemma OAI.CubicFirstMoment.angularHeat_inversion_of_lattice line 94