CubicThetaCoprimeShear.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An explicit finite-prime avoidance step for the level-nine Kubota multiplication proof. No prime-distribution theorem is required.

theorem OAI.CubicFirstMoment.cubicTheta_exists_coprime_shear line 14
Source documentation
Choose the shear by multiplying exactly the prime factors of f which do not divide a. This preserves all good residues and repairs the others.
```
theorem cubicTheta_exists_coprime_shear {a c f : Eisenstein}
    (hf : f ≠ 0) (hac : IsCoprime a (9*c)) :
    ∃ t : Eisenstein, (9:Eisenstein) ∣ t ∧ IsCoprime (a+t*c) f := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein