The finite set of bad primes of an integer hypersurface.
theorem
CCDN.ne_zero_of_irreducible_map
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
[CommSemiring R]
[CommSemiring S]
{φ : R →+* S}
{f : MvPolynomial σ R}
(h : Irreducible ((MvPolynomial.map φ) f))
:
A polynomial with an irreducible image under a coefficient map is nonzero.
@[reducible, inline]
Good reduction at a prime p: the reduction of f modulo p is nonzero and
absolutely irreducible.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CCDN.finite_hypersurface_bad_primes
{L : Type u_1}
{σ : Type u_2}
[Field L]
[CharZero L]
[IsAlgClosed L]
[Finite σ]
(f : MvPolynomial (Option σ) ℤ)
(hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f))
(hpos : 0 < f.totalDegree)
:
{p : ℕ | stepanovThreshold f.totalDegree < p ∧ HypersurfaceBadReduction f p}.Finite
Finiteness of the paper's bad-prime set above 27*d^4. A stronger set above d is finite; filtering it gives the exact prescribed cutoff.