p-integral polynomials #
GV p F 0 means that F ∈ ℚ[X] has p-integral coefficients. We show closure under powers,
composition and evaluation, and division by X - a (for p-integral roots a).
theorem
Zeta5Irrational.VG.eval
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{F : Polynomial ℚ}
{z : ℚ}
(hF : GV p F 0)
(hz : VG p z 0)
:
VG p (Polynomial.eval z F) 0
theorem
Zeta5Irrational.VG.eval_zero
{p : ℕ}
{F : Polynomial ℚ}
{r : ℚ}
(hF : GV p F r)
:
VG p (Polynomial.eval 0 F) r
theorem
Zeta5Irrational.GV.divByMonic_X_sub_C
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{F : Polynomial ℚ}
{a : ℚ}
(hF : GV p F 0)
(ha : VG p a 0)
:
GV p (F /ₘ (Polynomial.X - Polynomial.C a)) 0
theorem
Zeta5Irrational.factor_roots
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(ρs : Finset ℚ)
(hρ : ∀ ρ ∈ ρs, VG p ρ 0)
{F : Polynomial ℚ}
(hF : GV p F 0)
(hroot : ∀ ρ ∈ ρs, Polynomial.eval ρ F = 0)
:
∃ (S : Polynomial ℚ), GV p S 0 ∧ F = (∏ ρ ∈ ρs, (Polynomial.X - Polynomial.C ρ)) * S
An integral polynomial vanishing at p-integral distinct points is divisible by
∏ (X - ρ) with an integral quotient.
theorem
Zeta5Irrational.GV.multiset_prod
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(s : Multiset (Polynomial ℚ))
(b : Polynomial ℚ → ℚ)
(h : ∀ f ∈ s, GV p f (b f))
:
GV p s.prod (Multiset.map b s).sum
Multiset products.