Valuations of the polynomial moments

μ(t^e) = (-1)^e B_{2e+2} (2e+3)(2e+4)(2e+5)/24 has v_p ≥ -1 (p ≥ 5), and is p-integral for e < 2p - 3 (von Staudt–Clausen).

theorem Zeta5Irrational.VG_bernoulli_even {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) : VG p (bernoulli (2 * k)) (-1)

theorem Zeta5Irrational.VG_bernoulli_even_int {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) (hk : ¬p - 1 ∣ 2 * k) : VG p (bernoulli (2 * k)) 0

theorem Zeta5Irrational.VG_inv24 {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) : VG p 24⁻¹ 0

theorem Zeta5Irrational.VG_μmono {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (e : ℕ) : VG p (μmono e) (-1)

v_p(μ(t^e)) ≥ -1.

theorem Zeta5Irrational.VG_μmono_int {p : ℕ} [hp : Fact (Nat.Prime p)] (hp5 : 5 ≤ p) {e : ℕ} (he : e + 3 < 2 * p) : VG p (μmono e) 0

μ(t^e) is p-integral for e < 2p - 3.