OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimitiveRowFactorization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unique extraction of the primary common factor of a level-three row. The inverse uses a Bezout identity for its actual gcd.

  1. lemma OAI.CubicFirstMoment.cubicThetaFullRowMultiply_surjective line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaFullRow_factor_dvd line 48
  3. lemma OAI.CubicFirstMoment.cubicThetaFullRowMultiply_injective line 59
  4. def OAI.CubicFirstMoment.cubicThetaPrimitiveRowEquiv line 75