OAI/NumberTheory/CubicMoment/Theta/CubicThetaFreeCubeIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An exact bijection separating every primary cube factor into the part supported on the level and the free part. No multiplicity is lost.

  1. abbrev OAI.CubicFirstMoment.CubicThetaCoreIndex line 13
  2. abbrev OAI.CubicFirstMoment.CubicThetaFreeArgument line 15
  3. def OAI.CubicFirstMoment.cubicThetaFreeCubeJoin line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaFreeCubeJoin_injective line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaFreeCubeJoin_surjective line 43
  6. def OAI.CubicFirstMoment.cubicThetaFreeCubeEquiv line 64
  7. theorem OAI.CubicFirstMoment.cubicTheta_free_cube_tsum line 69