ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>Fintype F<VAR>Field F<VAR>hF : ringChar F ≠ 2<GOAL>2 ^ (Fintype.card F / 2) = ↑(ZMod.χ₈ ↑(Fintype.card F))
<VAR>ι : Type u_1<VAR>Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>Countable ι<VAR>a : ι → ℂ<VAR>q : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hq : ∀ (i : ι), a i = 0 ∨ 0 < q i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / q i ^ s.re<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>Countable ι<VAR>a : ι → ℂ<VAR>p : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hp : ∀ (i : ι), 0 ≤ p i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Set.Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / p i ^ s.re<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Set.Ioi 0, HasSum (fun i => if r i = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<GOAL>HasSum (fun i => s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))
<VAR>ι : Type u_1<VAR>Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
<GOAL>¬LSeriesSummable (fun n => ↑(ArithmeticFunction.moebius n)) 1
<VAR>s : ℂ<GOAL>LSeriesSummable (fun n => ↑(ArithmeticFunction.moebius n)) s ↔ 1 < s.re
<GOAL>(LSeries.abscissaOfAbsConv fun n => ↑(ArithmeticFunction.moebius n)) = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 n = ↑((fun x => ArithmeticFunction.zeta x) n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ℕ → R<GOAL>1 ⍟ f = (fun x => ↑(ArithmeticFunction.zeta x)) ⍟ f
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ℕ → R<GOAL>f ⍟ 1 = f ⍟ fun x => ↑(ArithmeticFunction.zeta x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>f g : ℕ → R<GOAL>(fun x => χ ↑x) * f ⍟ ((fun x => χ ↑x) * g) = (fun x => χ ↑x) * (f ⍟ g)
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<GOAL>(fun n_1 => χ ↑n_1) * δ = δ
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<GOAL>(δ * fun n_1 => χ ↑n_1) = δ
<VAR>n : ℕ<VAR>χ : DirichletCharacter ℂ n<GOAL>(fun n_1 => χ ↑n_1) ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(ArithmeticFunction.moebius n)) = δ
<VAR>χ : DirichletCharacter ℂ 0<GOAL>(fun n => χ ↑n) = δ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>χ : DirichletCharacter R 1<GOAL>(fun x => χ ↑x) = 1
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesSummable (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>hn : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<GOAL>(LSeries.abscissaOfAbsConv fun n => χ ↑n) = 1
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => χ ↑n) s * L ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.moebius n)) s = 1
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => χ ↑n) s ≠ 0
<GOAL>LSeries.abscissaOfAbsConv 1 = 1
<VAR>s : ℂ<GOAL>LSeriesSummable 1 s ↔ 1 < s.re
<GOAL>(L fun n => ↑(ArithmeticFunction.zeta n)) = L 1
<VAR>s : ℂ<GOAL>LSeriesSummable (fun x => ↑(ArithmeticFunction.zeta x)) s ↔ 1 < s.re
<GOAL>(LSeries.abscissaOfAbsConv fun n => ↑(ArithmeticFunction.zeta n)) = 1
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ArithmeticFunction.zeta n)) s = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun n => ↑(ArithmeticFunction.zeta n)) s (riemannZeta s)
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ArithmeticFunction.zeta n)) s * L (fun n => ↑(ArithmeticFunction.moebius n)) s = 1
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ArithmeticFunction.zeta n)) s ≠ 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L 1 s = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum 1 s (riemannZeta s)
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L 1 s * L (fun n => ↑(ArithmeticFunction.moebius n)) s = 1
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L 1 s ≠ 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>riemannZeta s ≠ 0
<GOAL>((fun n => ↑(ArithmeticFunction.vonMangoldt n)) ⍟ fun n => ↑(ArithmeticFunction.zeta n)) = fun n => Complex.log ↑n
<GOAL>(fun n => ↑(ArithmeticFunction.vonMangoldt n)) ⍟ 1 = fun n => Complex.log ↑n
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesSummable (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<GOAL>(((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) ⍟ fun n => χ ↑n) = (fun n => χ ↑n) * fun n => Complex.log ↑n
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv (L 1) s / L 1 s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv riemannZeta s / riemannZeta s
<VAR>d : ℤ<VAR>b : ℤ√d<GOAL>Pell.IsPell b ↔ b * star b = 1
<VAR>d : ℤ<VAR>b : ℤ√d<GOAL>Pell.IsPell b ↔ b ∈ unitary (ℤ√d)
<VAR>d : ℤ<VAR>b c : ℤ√d<VAR>hb : Pell.IsPell b<VAR>hc : Pell.IsPell c<GOAL>Pell.IsPell (b * c)
<VAR>d : ℤ<VAR>b : ℤ√d<GOAL>Pell.IsPell b ↔ Pell.IsPell (star b)
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>0 < Pell.d a1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.pell a1 n = (Pell.xn a1 n, Pell.yn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>Pell.xn a1 0 = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>Pell.yn a1 0 = 0
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xn a1 (n + 1) = Pell.xn a1 n * a + Pell.d a1 * Pell.yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yn a1 (n + 1) = Pell.xn a1 n + Pell.yn a1 n * a
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>Pell.xn a1 1 = a
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>Pell.yn a1 1 = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>0 < a * a
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>↑(Pell.d a1) = Pell.az a * Pell.az a - 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xz a1 (n + 1) = Pell.xz a1 n * Pell.az a + ↑(Pell.d a1) * Pell.yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yz a1 (n + 1) = Pell.xz a1 n + Pell.yz a1 n * Pell.az a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>(Pell.pellZd a1 n).re = ↑(Pell.xn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>(Pell.pellZd a1 n).im = ↑(Pell.yn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<GOAL>Pell.IsPell { re := ↑x, im := ↑y } ↔ x * x - Pell.d a1 * y * y = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.pellZd a1 (n + 1) = Pell.pellZd a1 n * { re := ↑a, im := 1 }
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>Pell.IsPell { re := ↑a, im := 1 }
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.IsPell (Pell.pellZd a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xz a1 n * Pell.xz a1 n - ↑(Pell.d a1) * Pell.yz a1 n * Pell.yz a1 n = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xn a1 n * Pell.xn a1 n - Pell.d a1 * Pell.yn a1 n * Pell.yn a1 n = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>a ^ n ≤ Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>n < a ^ n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>n < Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>0 < Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>b : ℤ√↑(Pell.d a1)<GOAL>1 ≤ b → Pell.IsPell b → b ≤ Pell.pellZd a1 n → ∃ n, b = Pell.pellZd a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>b : ℤ√↑(Pell.d a1)<VAR>b1 : 1 ≤ b<VAR>hp : Pell.IsPell b<GOAL>∃ n, b = Pell.pellZd a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>hp : x * x - Pell.d a1 * y * y = 1<GOAL>∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>Pell.pellZd a1 (m + n) = Pell.pellZd a1 m * Pell.pellZd a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>Pell.xn a1 (m + n) = Pell.xn a1 m * Pell.xn a1 n + Pell.d a1 * Pell.yn a1 m * Pell.yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>Pell.yn a1 (m + n) = Pell.xn a1 m * Pell.yn a1 n + Pell.yn a1 m * Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Pell.pellZd a1 (m - n) = Pell.pellZd a1 m * star (Pell.pellZd a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Pell.xz a1 (m - n) = Pell.xz a1 m * Pell.xz a1 n - ↑(Pell.d a1) * Pell.yz a1 m * Pell.yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Pell.yz a1 (m - n) = Pell.xz a1 n * Pell.yz a1 m - Pell.xz a1 m * Pell.yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>(Pell.xn a1 n).Coprime (Pell.yn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>StrictMono (Pell.yn a1)
<VAR>a : ℕ<VAR>a1 : 1 < a<GOAL>StrictMono (Pell.xn a1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>n ≤ Pell.yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<GOAL>Pell.yn a1 n ∣ Pell.yn a1 (n * k)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>Pell.yn a1 m ∣ Pell.yn a1 n ↔ m ∣ n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<GOAL>Pell.xn a1 (n * k) ≡ Pell.xn a1 n ^ k [MOD Pell.yn a1 n ^ 2] ∧ Pell.yn a1 (n * k) ≡ k * Pell.xn a1 n ^ (k - 1) * Pell.yn a1 n [MOD Pell.yn a1 n ^ 3]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yn a1 n * Pell.yn a1 n ∣ Pell.yn a1 (n * Pell.yn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n t : ℕ<VAR>h : Pell.yn a1 n * Pell.yn a1 n ∣ Pell.yn a1 t<GOAL>Pell.yn a1 n ∣ t
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.pellZd a1 (n + 2) + Pell.pellZd a1 n = ↑(2 * a) * Pell.pellZd a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1) ∧ Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.xz a1 (n + 2) = ↑(2 * a) * Pell.xz a1 (n + 1) - Pell.xz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yz a1 (n + 2) = ↑(2 * a) * Pell.yz a1 (n + 1) - Pell.yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yn a1 n ≡ n [MOD a - 1]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>Pell.yn a1 n ≡ n [MOD 2]
<VAR>y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ<GOAL>(a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y n : ℕ<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ Pell.yz a1 n * (↑a - ↑y) + ↑(y ^ n) - Pell.xz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>Pell.xn a1 n ∣ Pell.d a1 * Pell.yn a1 n * (Pell.yn a1 n * Pell.xn a1 j) + Pell.xn a1 j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>Pell.xn a1 (2 * n + j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ n<GOAL>Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<GOAL>Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>Pell.xn a1 (4 * n + j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<GOAL>Pell.xn a1 (4 * n - j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n j : ℕ<GOAL>i < j → j < n → Pell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>h : 2 * Pell.xn a1 n = Pell.xn a1 (n + 1)<GOAL>a = 2 ∧ n = 0
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<GOAL>i < j → j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → Pell.xn a1 i % Pell.xn a1 n < Pell.xn a1 j % Pell.xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ij : i ≤ j<VAR>j2n : j ≤ 2 * n<VAR>h : Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)<GOAL>i = j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>i2n : i ≤ 2 * n<VAR>j2n : j ≤ 2 * n<VAR>h : Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n]<VAR>ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)<GOAL>i = j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n]<GOAL>j = i ∨ j + i = 4 * n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n]<GOAL>j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n]
<VAR>a b c : ℕ<VAR>a1 : 1 < a<VAR>b1 : 1 < b<VAR>h : a ≡ b [MOD c]<VAR>n : ℕ<GOAL>Pell.xn a1 n ≡ Pell.xn b1 n [MOD c] ∧ Pell.yn a1 n ≡ Pell.yn b1 n [MOD c]
<VAR>a k x y : ℕ<GOAL>(∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔ 1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ u v s t b, x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
<VAR>a y k : ℕ<VAR>hy0 : y ≠ 0<VAR>hk0 : k ≠ 0<VAR>hyk : y ^ k < a<GOAL>↑(y ^ k) < 2 * ↑a * ↑y - ↑y * ↑y - 1
<VAR>m n k : ℕ<GOAL>n ^ k = m ↔ k = 0 ∧ m = 1 ∨ 0 < k ∧ (n = 0 ∧ m = 0 ∨ 0 < n ∧ ∃ w a t z, ∃ (a1 : 1 < a), Pell.xn a1 k ≡ Pell.yn a1 k * (a - n) + m [MOD t] ∧ 2 * a * n = t + (n * n + 1) ∧ m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>Disjoint {x | ∃ k, beattySeq r k = x} {x | ∃ k, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>¬∃ j k m, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1 ∧ ↑m ≤ ↑j / s ∧ (↑j + 1) / s < ↑m + 1
<VAR>r : ℝ<VAR>j : ℤ<VAR>h : r > 0<GOAL>j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1
<VAR>r : ℝ<VAR>j : ℤ<VAR>h : r > 0<GOAL>j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}
<VAR>r : ℝ<VAR>hr : Irrational r<GOAL>{x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}
<VAR>p : ℕ<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>padicNorm p q = ↑p ^ (-padicValRat p q)
<VAR>p : ℕ<VAR>q : ℚ<GOAL>0 ≤ padicNorm p q
<VAR>p : ℕ<GOAL>padicNorm p 0 = 0
<VAR>p : ℕ<GOAL>padicNorm p 1 = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>padicNorm p ↑p = (↑p)⁻¹
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>padicNorm p ↑p < 1
<VAR>p : ℕ<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>∃ z, padicNorm p q = ↑p ^ (-z)
<VAR>p : ℕ<VAR>q : ℚ<GOAL>padicNorm p (-q) = padicNorm p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>padicNorm p (q * r) = padicNorm p q * padicNorm p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>padicNorm p (q / r) = padicNorm p q / padicNorm p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<GOAL>padicNorm p ↑z ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hne : padicNorm p q ≠ padicNorm p r<GOAL>padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>z : ℤ<GOAL>↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℕ<GOAL>padicNorm p ↑m ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℕ<GOAL>padicNorm p ↑m < 1 ↔ p ∣ m
<VAR>p : ℕ<VAR>a : ℚ<VAR>hp : Fact (Nat.Prime p)<VAR>H : 1 < padicNorm p a<GOAL>¬a.isInt = true
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<GOAL>s.Nonempty → (∀ i ∈ s, padicNorm p (F i) < t) → padicNorm p (∑ i ∈ s, F i) < t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<GOAL>s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t
<VAR>R : Type u_1<VAR>n : ℕ<VAR>CommRing R<VAR>x y p : R<VAR>h : p ∣ x - y<GOAL>p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>CommRing R<VAR>x y p : R<VAR>h : p ∣ x - y<GOAL>p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>CommRing R<VAR>x y : R<VAR>h : ↑n ∣ x - y<GOAL>↑n ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p x : R<VAR>n : ℕ<GOAL>p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>CommRing R<VAR>x y p : R<VAR>hp : Prime p<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>hn : ¬p ∣ ↑n<GOAL>¬p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<VAR>p : ℕ<VAR>hp : Odd p<GOAL>↑p ^ 2 ∣ ∑ i ∈ Finset.range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p : R<VAR>hp : Prime p<VAR>x y : R<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : ¬p ∣ ↑n<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>p : ℕ<VAR>IsDomain R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>multiplicity (↑p) (∑ i ∈ Finset.range p, x ^ i * y ^ (p - 1 - i)) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>p : ℕ<VAR>IsDomain R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>multiplicity (↑p) (x ^ p - y ^ p) = multiplicity (↑p) (x - y) + 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>p : ℕ<VAR>IsDomain R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>a : ℕ<GOAL>multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<GOAL>multiplicity (↑p) (x ^ n - y ^ n) = multiplicity (↑p) (x - y) + multiplicity p n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x + y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity (↑p) (x ^ n + y ^ n) = multiplicity (↑p) (x + y) + multiplicity p n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℕ<VAR>hxy : p ∣ x + y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>multiplicity p (x ^ n + y ^ n) = multiplicity p (x + y) + multiplicity p n
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>n : ℕ<GOAL>x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ Finset.range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
<VAR>x : ℤ<GOAL>Odd x → x ^ 2 % 4 = 1
<VAR>x y : ℤ<VAR>hx : ¬2 ∣ x<VAR>hxy : 4 ∣ x - y<VAR>i : ℕ<GOAL>multiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<GOAL>multiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = multiplicity 2 (x - y) + ↑n
<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<GOAL>multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hn : Even n<GOAL>multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>x y : ℕ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : Even n<GOAL>multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
<VAR>x y : ℕ<VAR>hyx : y < x<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hneven : Even n<GOAL>padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n
<VAR>x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n
<VAR>x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hxy : p ∣ x + y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : Odd n<GOAL>padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n
<VAR>n : ℕ<GOAL>padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : K<GOAL>NumberField.house α = ↑(Finset.univ.sup' ⋯ fun φ => ‖φ α‖₊)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>α : ι → K<GOAL>NumberField.house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, NumberField.house (α i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : K<GOAL>0 ≤ NumberField.house α
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α β : K<GOAL>NumberField.house (α * β) ≤ NumberField.house α * NumberField.house β
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ℤ<GOAL>NumberField.house ↑x = ↑|x|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<GOAL>0 ≤ NumberField.house.c K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<VAR>α : NumberField.RingOfIntegers K<VAR>i : K →+* ℂ<GOAL>Complex.abs ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr ↑α) i) ≤ NumberField.house.c K * NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) α)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>0 ≤ NumberField.house.supOfBasis K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : Type u_2<VAR>β : Type u_3<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>ha : a ≠ 0<GOAL>NumberField.house.asiegel K a ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>β : Type u_3<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<GOAL>NumberField.house.ξ K x ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : Type u_2<VAR>β : Type u_3<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>l : β<VAR>k : α<VAR>r : K →+* ℂ<GOAL>a k l * (NumberField.house.newBasis K) r = ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype β<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : (NumberField.house.asiegel K a).mulVec x = 0<GOAL>a.mulVec (NumberField.house.ξ K x) = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<GOAL>0 ≤ NumberField.house.c₂ K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>Fintype β<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<GOAL>‖NumberField.house.asiegel K a‖ ≤ NumberField.house.c₂ K * A
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>Fintype β<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>p q : ℕ<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(FiniteDimensional.finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<VAR>l : β<GOAL>NumberField.house ↑(NumberField.house.ξ K x l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>Fintype β<VAR>a : Matrix α β (NumberField.RingOfIntegers K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A<GOAL>∃ ξ, ξ ≠ 0 ∧ a.mulVec ξ = 0 ∧ ∀ (l : β), NumberField.house ↑(ξ l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
<VAR>α : Type u_1<VAR>f : (α → ℕ) → ℤ<GOAL>IsPoly f → IsPoly (-f)