Module

SchurPrimeDivisors.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SchurPrimeDivisors

2 declarations indexed from sourceView source ↗

Module documentation

New prime divisors of integer-polynomial values

A nonconstant integer polynomial has a nonzero value A. On any progression through that argument with step A times the product P of forbidden primes, its values have shape A (1 + Pb). Finite fibres allow a value different from 0, A and -A. A prime divisor of the second factor is therefore new. This is the elementary Schur argument and does not invoke prime density.

Imports9

Mathlib.Algebra.Polynomial.Roots
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Mathlib.Order.Filter.TendstoCofinite
Mathlib.Data.Nat.Prime.Defs
Mathlib.Data.Int.Basic
Mathlib.Data.Set.Finite.Basic
Mathlib.Tactic.Ring

Imported by2

theorem

exists_prime_not_mem_dvd_eval

L33 ↗

AlgebraicNumberTheory.PrimeSelection.exists_prime_not_mem_dvd_eval

Documentation

A nonconstant integer polynomial has a nonzero value with a prime factor outside any prescribed finite set of natural numbers.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem exists_prime_not_mem_dvd_eval
    (f : Polynomial ℤ) (hf : f.natDegree ≠ 0) (S : Finset ℕ) :
    ∃ q : ℕ, q.Prime ∧ q ∉ S ∧
      ∃ n : ℤ, f.eval n ≠ 0 ∧ (q : ℤ) ∣ f.eval n

theorem

infinite_primes_dvd_nonzero_eval

L106 ↗

AlgebraicNumberTheory.PrimeSelection.infinite_primes_dvd_nonzero_eval