OAI/NumberTheory/CubicMoment/Theta/CubicThetaUnitLifting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unit lifting through powers of an Eisenstein modulus. The cardinality factor is obtained from the actual additive and multiplicative kernels.

  1. def OAI.CubicFirstMoment.unitKernelEquivAddKernel line 10
  2. lemma OAI.CubicFirstMoment.unit_card_mul_of_reflect line 40
  3. lemma OAI.CubicFirstMoment.cubicTheta_residue_mk_isUnit_iff line 54
  4. lemma OAI.CubicFirstMoment.cubicTheta_unit_card_lift line 58
  5. lemma OAI.CubicFirstMoment.cubicTheta_power_units_card line 72
  6. lemma OAI.CubicFirstMoment.cubicTheta_three_units_card line 83