CubicThetaFactorUniqueness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the primary squarefree-times-cube coordinates in the published cubic theta coefficient formulas.

theorem OAI.CubicFirstMoment.primary_squarefree_cube_unique line 13
Source documentation
Primary normalization removes the cube-root unit ambiguity, and the squarefree exponent is the residue modulo three of each prime valuation.
```
theorem primary_squarefree_cube_unique {c d c' d' : Eisenstein}
    (hc : primary c) (hd : primary d) (hc' : primary c') (hd' : primary d')
    (hcs : Squarefree c) (hcs' : Squarefree c') (he : c*d^3 = c'*d'^3) :
    c = c' ∧ d = d' := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary