OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCosetPermutation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Right translation permutes the actual finite right transversal of the prime covering subgroup. The left factor remains in that subgroup.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCosetStep line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCosetStep_cancel line 15
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCosetPermutation line 31
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCosetPermutation_factor line 39