ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>f g : (α → ℕ) → ℤ<VAR>hf : IsPoly f<VAR>hg : IsPoly g<GOAL>IsPoly (f + g)
<VAR>α : Type u_1<VAR>f : Poly α<GOAL>IsPoly ⇑f
<VAR>α : Type u_1<VAR>f g : Poly α<GOAL>(∀ (x : α → ℕ), f x = g x) → f = g
<VAR>α : Type u_1<VAR>i : α<VAR>x : α → ℕ<GOAL>(Poly.proj i) x = ↑(x i)
<VAR>α : Type u_1<VAR>n : ℤ<VAR>x : α → ℕ<GOAL>(Poly.const n) x = n
<VAR>α : Type u_1<GOAL>⇑0 = ⇑(Poly.const 0)
<VAR>α : Type u_1<GOAL>⇑1 = ⇑(Poly.const 1)
<VAR>α : Type u_1<VAR>f : Poly α<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u_1<VAR>f g : Poly α<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_1<VAR>f g : Poly α<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u_1<VAR>f g : Poly α<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u_1<VAR>x : α → ℕ<GOAL>0 x = 0
<VAR>α : Type u_1<VAR>x : α → ℕ<GOAL>1 x = 1
<VAR>α : Type u_1<VAR>f : Poly α<VAR>x : α → ℕ<GOAL>(-f) x = -f x
<VAR>α : Type u_1<VAR>f g : Poly α<VAR>x : α → ℕ<GOAL>(f + g) x = f x + g x
<VAR>α : Type u_1<VAR>f g : Poly α<VAR>x : α → ℕ<GOAL>(f - g) x = f x - g x
<VAR>α : Type u_1<VAR>f g : Poly α<VAR>x : α → ℕ<GOAL>(f * g) x = f x * g x
<VAR>α : Type u_1<VAR>C : Poly α → Prop<VAR>H1 : ∀ (i : α), C (Poly.proj i)<VAR>H2 : ∀ (n : ℤ), C (Poly.const n)<VAR>H3 : ∀ (f g : Poly α), C f → C g → C (f - g)<VAR>H4 : ∀ (f g : Poly α), C f → C g → C (f * g)<VAR>f : Poly α<GOAL>C f
<VAR>α : Type u_1<VAR>x : α → ℕ<VAR>l : List (Poly α)<GOAL>0 ≤ (Poly.sumsq l) x
<VAR>α : Type u_1<VAR>x : α → ℕ<VAR>l : List (Poly α)<GOAL>(Poly.sumsq l) x = 0 ↔ List.Forall (fun a => a x = 0) l
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>g : Poly α<VAR>v : β → ℕ<GOAL>(Poly.map f g) v = g (v ∘ f)
<VAR>α : Type u<VAR>S S' : Set (α → ℕ)<VAR>d : Dioph S<VAR>H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'<GOAL>Dioph S'
<VAR>α : Type u<VAR>S : Set (α → ℕ)<VAR>p : Poly α<VAR>h : ∀ (v : α → ℕ), S v ↔ p v = 0<GOAL>Dioph S
<VAR>α β γ : Type u<VAR>f : β → γ<VAR>g : γ → Option β<VAR>inv : ∀ (x : β), g (f x) = some x<VAR>p : Poly (α ⊕ β)<VAR>v : α → ℕ<GOAL>(∃ t, p (v ⊗ t) = 0) ↔ ∃ t, (Poly.map (Sum.inl ⊗ Sum.inr ∘ f) p) (v ⊗ t) = 0
<VAR>α β γ : Type u<VAR>S : Set (α → ℕ)<VAR>f : β → γ<VAR>g : γ → Option β<VAR>inv : ∀ (x : β), g (f x) = some x<VAR>p : Poly (α ⊕ β)<VAR>h : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<GOAL>∃ q, ∀ (v : α → ℕ), S v ↔ ∃ t, q (v ⊗ t) = 0
<VAR>α : Type u<VAR>β : Type u<VAR>S : Set (α → ℕ)<VAR>f : α → β<GOAL>Dioph S → Dioph {v | v ∘ f ∈ S}
<VAR>α : Type u<VAR>l : List (Set (α → ℕ))<VAR>d : List.Forall Dioph l<GOAL>Dioph {v | List.Forall (fun S => v ∈ S) l}
<VAR>α : Type u<VAR>S S' : Set (α → ℕ)<VAR>d : Dioph S<VAR>d' : Dioph S'<GOAL>Dioph (S ∩ S')
<VAR>α : Type u<VAR>S S' : Set (α → ℕ)<GOAL>Dioph S → Dioph S' → Dioph (S ∪ S')
<VAR>α β : Type u<VAR>f : (α → ℕ) → ℕ<VAR>g : α → β<VAR>d : Dioph.DiophFn f<GOAL>Dioph.DiophFn fun v => f (v ∘ g)
<VAR>α β : Type u<VAR>S : Set (α ⊕ β → ℕ)<GOAL>Dioph S → Dioph {v | ∃ x, v ⊗ x ∈ S}
<VAR>α : Type u<VAR>S : Set (Option α → ℕ)<GOAL>Dioph S → Dioph {v | ∃ x, x ::ₒ v ∈ S}
<VAR>α : Type u<VAR>f : (α → ℕ) →. ℕ<VAR>d : Dioph.DiophPFun f<GOAL>Dioph f.Dom
<VAR>α : Type u<VAR>f : (α → ℕ) → ℕ<GOAL>Dioph.DiophFn f = Dioph.DiophPFun ↑f
<VAR>α : Type u<VAR>p : Poly α<GOAL>Dioph.DiophFn fun v => (p v).natAbs
<VAR>α : Type u<VAR>i : α<GOAL>Dioph.DiophFn fun v => v i
<VAR>α : Type u<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) →. ℕ<VAR>df : Dioph.DiophPFun f<GOAL>Dioph {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
<VAR>α : Type u<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<GOAL>Dioph {v | f v ::ₒ v ∈ S}
<VAR>n : ℕ<VAR>S : Set (Vector3 ℕ n.succ)<VAR>d : Dioph S<VAR>f : Vector3 ℕ n → ℕ<VAR>df : Dioph.DiophFn f<GOAL>Dioph {v | Vector3.cons (f v) v ∈ S}
<VAR>n : ℕ<VAR>S : Set (Vector3 ℕ n.succ)<VAR>d : Dioph S<GOAL>Dioph {v | ∃ x, Vector3.cons x v ∈ S}
<VAR>n : ℕ<VAR>f : Vector3 ℕ n → ℕ<GOAL>Dioph.DiophFn f ↔ Dioph {v | f (v ∘ Fin2.fs) = v Fin2.fz}
<VAR>n : ℕ<VAR>f : Vector3 ℕ n →. ℕ<GOAL>Dioph.DiophPFun f ↔ Dioph {v | f.graph (v ∘ Fin2.fs, v Fin2.fz)}
<VAR>α : Type<VAR>n : ℕ<VAR>S : Set (α ⊕ Fin2 n → ℕ)<GOAL>Dioph S → ∀ {f : Vector3 ((α → ℕ) → ℕ) n}, VectorAllP Dioph.DiophFn f → Dioph {v | (v ⊗ fun i => f i v) ∈ S}
<VAR>α : Type<VAR>n : ℕ<VAR>S : Set (Vector3 ℕ n)<VAR>d : Dioph S<VAR>f : Vector3 ((α → ℕ) → ℕ) n<VAR>df : VectorAllP Dioph.DiophFn f<GOAL>Dioph {v | (fun i => f i v) ∈ S}
<VAR>α : Type<VAR>n : ℕ<VAR>f : Vector3 ℕ n → ℕ<VAR>df : Dioph.DiophFn f<VAR>g : Vector3 ((α → ℕ) → ℕ) n<VAR>dg : VectorAllP Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f fun i => g i v
<VAR>n : ℕ<VAR>m : ℕ<VAR>Fin2.IsLT m n<GOAL>Dioph.DiophFn fun v => v (Fin2.ofNat' m)
<VAR>α : Type<VAR>n : ℕ<GOAL>Dioph.DiophFn (Function.const (α → ℕ) n)
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<VAR>S : ℕ → ℕ → Prop<VAR>d : Dioph fun v => S (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))<GOAL>Dioph fun v => S (f v) (g v)
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<VAR>h : ℕ → ℕ → ℕ<VAR>d : Dioph.DiophFn fun v => h (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))<GOAL>Dioph.DiophFn fun v => h (f v) (g v)
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph fun v => f v = g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v + g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v * g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph {v | f v ≤ g v}
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph {v | f v < g v}
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph {v | f v ≠ g v}
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v - g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph fun v => f v ∣ g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v % g v
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<VAR>h : (α → ℕ) → ℕ<VAR>dh : Dioph.DiophFn h<GOAL>Dioph fun v => f v ≡ g v [MOD h v]
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v / g v
<GOAL>Dioph fun v => ∃ (h : 1 < v (Fin2.ofNat' 0)), Pell.xn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 2) ∧ Pell.yn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 3)
<GOAL>Dioph.DiophPFun fun v => { Dom := 1 < v (Fin2.ofNat' 0), get := fun h => Pell.xn h (v (Fin2.ofNat' 1)) }
<VAR>α : Type<VAR>f g : (α → ℕ) → ℕ<VAR>df : Dioph.DiophFn f<VAR>dg : Dioph.DiophFn g<GOAL>Dioph.DiophFn fun v => f v ^ g v
<VAR>z : ZMod 4<GOAL>z * z ≠ 2
<VAR>z : ℤ<GOAL>z * z % 4 ≠ 2
<VAR>x y z : ℤ<GOAL>PythagoreanTriple x y z ↔ PythagoreanTriple y x z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<GOAL>x * x + y * y = z * z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>k : ℤ<GOAL>PythagoreanTriple (k * x) (k * y) (k * z)
<VAR>x y z : ℤ<VAR>k : ℤ<VAR>hk : k ≠ 0<GOAL>PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>k : ℤ<VAR>hc : h.IsClassified<GOAL>⋯.IsClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<GOAL>↑(x.gcd y) ∣ z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<GOAL>PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hp : h.IsPrimitiveClassified<GOAL>h.IsClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>z ≠ 0
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hx : x = 0<GOAL>h.IsPrimitiveClassified
<VAR>K : Type u_1<VAR>Field K<VAR>hk : ∀ (x : K), 1 + x ^ 2 ≠ 0<VAR>x : K<GOAL>↑((circleEquivGen hk) x) = (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2))
<VAR>K : Type u_1<VAR>Field K<VAR>hk : ∀ (x : K), 1 + x ^ 2 ≠ 0<VAR>v : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }<GOAL>(circleEquivGen hk).symm v = (↑v).1 / ((↑v).2 + 1)
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hm : m % 2 = 0<VAR>hn : n % 2 = 1<GOAL>(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
<VAR>m n : ℤ<VAR>h : m.gcd n = 1<VAR>hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<GOAL>(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<GOAL>h.IsClassified
<VAR>x y z : ℤ<GOAL>PythagoreanTriple x y z ∧ x.gcd y = 1 ↔ ∃ m n, (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h_coprime : x.gcd y = 1<VAR>h_parity : x % 2 = 1<VAR>h_pos : 0 < z<GOAL>∃ m n, x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
<VAR>x y z : ℤ<GOAL>PythagoreanTriple x y z ↔ ∃ k m n, (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
<VAR>n : ℕ<GOAL>harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹
<VAR>n : ℕ<VAR>Hn : n ≠ 0<GOAL>0 < harmonic n
<VAR>Fq F : Type<VAR>Field Fq<VAR>Field F<VAR>Fqt : Type u_1<VAR>Field Fqt<VAR>Algebra Fq[X] Fqt<VAR>IsFractionRing Fq[X] Fqt<VAR>Algebra (RatFunc Fq) F<VAR>Algebra Fqt F<VAR>Algebra Fq[X] F<VAR>IsScalarTower Fq[X] Fqt F<VAR>IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>FunctionField Fq F ↔ FiniteDimensional Fqt F
<VAR>Fq F : Type<VAR>Field Fq<VAR>Field F<VAR>Algebra Fq[X] F<VAR>Algebra (RatFunc Fq) F<VAR>IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>Function.Injective ⇑(algebraMap Fq[X] F)
<VAR>Fq F : Type<VAR>Field Fq<VAR>Field F<VAR>Algebra Fq[X] F<VAR>Algebra (RatFunc Fq) F<VAR>IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>Function.Injective ⇑(algebraMap Fq[X] ↥(FunctionField.ringOfIntegers Fq F))
<VAR>Fq F : Type<VAR>Field Fq<VAR>Field F<VAR>Algebra Fq[X] F<VAR>Algebra (RatFunc Fq) F<VAR>IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>¬IsField ↥(FunctionField.ringOfIntegers Fq F)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<GOAL>FunctionField.inftyValuationDef Fq 0 = 0
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<GOAL>FunctionField.inftyValuationDef Fq 1 = 1
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x y : RatFunc Fq<GOAL>FunctionField.inftyValuationDef Fq (x * y) = FunctionField.inftyValuationDef Fq x * FunctionField.inftyValuationDef Fq y
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x y : RatFunc Fq<GOAL>FunctionField.inftyValuationDef Fq (x + y) ≤ max (FunctionField.inftyValuationDef Fq x) (FunctionField.inftyValuationDef Fq y)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x : RatFunc Fq<VAR>hx : x ≠ 0<GOAL>FunctionField.inftyValuationDef Fq x = ↑(Multiplicative.ofAdd x.intDegree)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x : RatFunc Fq<GOAL>(FunctionField.inftyValuation Fq) x = FunctionField.inftyValuationDef Fq x
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>k : Fq<VAR>hk : k ≠ 0<GOAL>FunctionField.inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<GOAL>FunctionField.inftyValuationDef Fq RatFunc.X = ↑(Multiplicative.ofAdd 1)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>p : Fq[X]<VAR>hp : p ≠ 0<GOAL>FunctionField.inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x : RatFunc Fq<GOAL>Valued.v x = FunctionField.inftyValuationDef Fq x
<VAR>Fq : Type<VAR>Field Fq<VAR>DecidableEq (RatFunc Fq)<VAR>x : FunctionField.FqtInfty Fq<GOAL>Valued.v x = Valued.extension x
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.hurwitzZetaOdd (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.hurwitzZeta (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.hurwitzZeta (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Set.Icc 0 1<GOAL>HurwitzZeta.hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
<VAR>n : ℕ<GOAL>Real.log ↑(n + 1) ≤ ↑(harmonic n)
<VAR>n : ℕ<GOAL>↑(harmonic n) ≤ 1 + Real.log ↑n
<VAR>y : ℝ<VAR>hy : 0 ≤ y<GOAL>Real.log y ≤ ↑(harmonic ⌊y⌋₊)
<VAR>k : ℕ<VAR>n : ℕ<VAR>hk0 : k ≠ 0<GOAL>∃ p, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k : ℕ<VAR>hk0 : k ≠ 0<GOAL>∃ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p ∧ p ≡ 1 [MOD k]
<VAR>k : ℕ<VAR>hk0 : k ≠ 0<GOAL>{p | Nat.Prime p ∧ p ≡ 1 [MOD k]}.Infinite
<VAR>p q : ℕ<GOAL>mersenne p < mersenne q ↔ p < q
<VAR>p q : ℕ<GOAL>mersenne p ≤ mersenne q ↔ p ≤ q
<VAR>p : ℕ<GOAL>0 < mersenne p ↔ 0 < p
<VAR>p : ℕ<GOAL>1 < mersenne p ↔ 1 < p
<VAR>p : ℕ<VAR>hp : p ≠ 0<GOAL>0 < 2 ^ p - 1
<VAR>p : ℕ<VAR>hp : p ≠ 0<GOAL>2 ^ p - 1 ≠ 0
<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>i : ℕ<GOAL>0 ≤ LucasLehmer.sMod p i
<VAR>p i : ℕ<GOAL>LucasLehmer.sMod p i % (2 ^ p - 1) = LucasLehmer.sMod p i
<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>i : ℕ<GOAL>LucasLehmer.sMod p i < 2 ^ p - 1
<VAR>p' i : ℕ<GOAL>LucasLehmer.sZMod (p' + 2) i = ↑(LucasLehmer.s i)
<VAR>p : ℕ<GOAL>↑(2 ^ p - 1) = 2 ^ p - 1
<VAR>p i : ℕ<GOAL>LucasLehmer.sZMod p i = ↑(LucasLehmer.sMod p i)
<VAR>p : ℕ<VAR>w : 1 < p<GOAL>lucasLehmerResidue p = 0 ↔ LucasLehmer.sMod p (p - 2) = 0
<VAR>q : ℕ+<VAR>x y : LucasLehmer.X q<VAR>h₁ : x.1 = y.1<VAR>h₂ : x.2 = y.2<GOAL>x = y
<VAR>q : ℕ+<GOAL>0.1 = 0
<VAR>q : ℕ+<GOAL>0.2 = 0
<VAR>q : ℕ+<VAR>x y : LucasLehmer.X q<GOAL>(x + y).1 = x.1 + y.1
<VAR>q : ℕ+<VAR>x y : LucasLehmer.X q<GOAL>(x + y).2 = x.2 + y.2
<VAR>q : ℕ+<VAR>x : LucasLehmer.X q<GOAL>(-x).1 = -x.1
<VAR>q : ℕ+<VAR>x : LucasLehmer.X q<GOAL>(-x).2 = -x.2
<VAR>q : ℕ+<VAR>x y : LucasLehmer.X q<GOAL>(x * y).1 = x.1 * y.1 + 3 * x.2 * y.2
<VAR>q : ℕ+<VAR>x y : LucasLehmer.X q<GOAL>(x * y).2 = x.1 * y.2 + x.2 * y.1
<VAR>q : ℕ+<GOAL>1.1 = 1
<VAR>q : ℕ+<GOAL>1.2 = 0
<VAR>q : ℕ+<VAR>n : ℕ<GOAL>(↑n).1 = ↑n
<VAR>q : ℕ+<VAR>n : ℕ<GOAL>(↑n).2 = 0
<VAR>q : ℕ+<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).1 = OfNat.ofNat n
<VAR>q : ℕ+<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).2 = 0
<VAR>q : ℕ+<VAR>x y z : LucasLehmer.X q<GOAL>x * (y + z) = x * y + x * z
<VAR>q : ℕ+<VAR>x y z : LucasLehmer.X q<GOAL>(x + y) * z = x * z + y * z
<VAR>q : ℕ+<VAR>n : ℤ<GOAL>(↑n).1 = ↑n
<VAR>q : ℕ+<VAR>n : ℤ<GOAL>(↑n).2 = 0
<VAR>q : ℕ+<VAR>n m : ℤ<GOAL>↑(n * m) = ↑n * ↑m
<VAR>q : ℕ+<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>q : ℕ+<GOAL>Fintype.card (LucasLehmer.X q) = ↑q ^ 2
<VAR>q : ℕ+<VAR>w : 1 < q<GOAL>Fintype.card (LucasLehmer.X q)ˣ < ↑q ^ 2
<VAR>q : ℕ+<GOAL>LucasLehmer.X.ω * LucasLehmer.X.ωb = 1
<VAR>q : ℕ+<GOAL>LucasLehmer.X.ωb * LucasLehmer.X.ω = 1
<VAR>q : ℕ+<VAR>i : ℕ<GOAL>↑(LucasLehmer.s i) = LucasLehmer.X.ω ^ 2 ^ i + LucasLehmer.X.ωb ^ 2 ^ i
<VAR>p' : ℕ<GOAL>2 < LucasLehmer.q (p' + 2)
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>∃ k, LucasLehmer.X.ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * LucasLehmer.X.ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>LucasLehmer.X.ω ^ 2 ^ (p' + 1) = -1
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>LucasLehmer.X.ω ^ 2 ^ (p' + 2) = 1
<VAR>p : ℕ<GOAL>↑(LucasLehmer.ωUnit p) = LucasLehmer.X.ω
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>orderOf (LucasLehmer.ωUnit (p' + 2)) = 2 ^ (p' + 2)
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>2 ^ (p' + 2) < ↑(LucasLehmer.q (p' + 2)) ^ 2
<VAR>p : ℕ<VAR>w : 1 < p<GOAL>LucasLehmerTest p → Nat.Prime (mersenne p)
<VAR>p k : ℕ<VAR>hp : 2 ≤ p<GOAL>↑(LucasLehmer.norm_num_ext.sMod' (2 ^ p - 1) k) = LucasLehmer.sMod p k
<VAR>p : ℕ<VAR>hp : Nat.blt 1 p = true<VAR>h : LucasLehmer.norm_num_ext.sMod' (2 ^ p - 1) (p - 2) = 0<GOAL>LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : Nat.blt 1 p = true<VAR>h : Nat.ble 1 (LucasLehmer.norm_num_ext.sMod' (2 ^ p - 1) (p - 2)) = true<GOAL>¬LucasLehmerTest p
<VAR>p np : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat p np → LucasLehmerTest np → LucasLehmerTest p
<VAR>p np : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat p np → ¬LucasLehmerTest np → ¬LucasLehmerTest p
<VAR>n k : ℕ<GOAL>k ≡ k / 2 ^ n + k % 2 ^ n [MOD 2 ^ n - 1]
<GOAL>1 / 2 < Real.eulerMascheroniSeq 6
<GOAL>Real.eulerMascheroniSeq' 1 = 1
<GOAL>Real.eulerMascheroniSeq' 6 < 2 / 3
<VAR>m n : ℕ<GOAL>Real.eulerMascheroniSeq m < Real.eulerMascheroniSeq' n
<GOAL>Filter.Tendsto Real.eulerMascheroniSeq Filter.atTop (𝓝 Real.eulerMascheroniConstant)
<GOAL>Filter.Tendsto (fun n => ↑(harmonic n) - Real.log (↑n + 1)) Filter.atTop (𝓝 Real.eulerMascheroniConstant)
<GOAL>Filter.Tendsto Real.eulerMascheroniSeq' Filter.atTop (𝓝 Real.eulerMascheroniConstant)
<GOAL>Filter.Tendsto (fun n => ↑(harmonic n) - Real.log ↑n) Filter.atTop (𝓝 Real.eulerMascheroniConstant)
<VAR>n : ℕ<GOAL>Real.eulerMascheroniSeq n < Real.eulerMascheroniConstant
<VAR>n : ℕ<GOAL>Real.eulerMascheroniConstant < Real.eulerMascheroniSeq' n
<GOAL>1 / 2 < Real.eulerMascheroniConstant
<GOAL>Real.eulerMascheroniConstant < 2 / 3
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommMonoid R<VAR>CommMonoidWithZero R'<VAR>g : Rˣ<VAR>hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g<VAR>χ₁ χ₂ : MulChar R R'<GOAL>χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommRing R<VAR>CommRing R'<VAR>StarRing R'<VAR>χ : MulChar R R'<VAR>a : R<GOAL>χ.starComp a = (starRingEnd R') (χ a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommRing R<VAR>CommRing R'<VAR>StarRing R'<VAR>χ : MulChar R R'<VAR>a : R<GOAL>(star χ) a = star (χ a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommRing R<VAR>CommRing R'<VAR>Fintype Rˣ<VAR>a : Rˣ<VAR>χ : MulChar R R'<GOAL>(MulChar.equivToUnitHom χ) a ∈ rootsOfUnity ⟨Fintype.card Rˣ, ⋯⟩ R'
<VAR>R : Type u_1<VAR>CommRing R<VAR>Finite Rˣ<VAR>χ : MulChar R ℂ<GOAL>star χ = χ⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>Finite Rˣ<VAR>χ : MulChar R ℂ<VAR>a : R<GOAL>star (χ a) = χ⁻¹ a
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>Fintype M<VAR>DecidableEq M<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>ζ : Rˣ<VAR>hζ : ζ ∈ rootsOfUnity (MulChar.Monoid.orderUnits M) R<VAR>g : Mˣ<VAR>hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g<GOAL>(MulChar.ofRootOfUnity hζ hg) ↑g = ↑ζ
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>R : Type u_2<VAR>CommRing R<VAR>n : ℕ<VAR>h : n ∣ Fintype.card F - 1<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>∃ χ, orderOf χ = n
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>R : Type u_2<VAR>CommRing R<VAR>χ : MulChar F R<GOAL>orderOf χ ∣ Fintype.card F - 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>R : Type u_2<VAR>CommRing R<VAR>DecidableEq F<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ ↑(MulChar.Monoid.orderUnits F)<GOAL>∃ χ, orderOf χ = Fintype.card Fˣ
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>R : Type u_2<VAR>CommRing R<VAR>χ : MulChar F R<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ ζ ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>R : Type u_2<VAR>CommRing R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ ζ ∈ rootsOfUnity ⟨n, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ k < n, χ a = μ ^ k
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<GOAL>χ a ∈ Algebra.adjoin ℤ {μ}
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>χ : MulChar F R<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (orderOf χ)<VAR>a : F<GOAL>χ a ∈ Algebra.adjoin ℤ {μ}
<VAR>p : ℕ<GOAL>padicValNat p 0 = 0
<VAR>p : ℕ<GOAL>padicValNat p 1 = 0
<VAR>p n : ℕ<VAR>h : ¬p ∣ n<GOAL>padicValNat p n = 0
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<GOAL>↑(p.maxPowDiv n) = multiplicity p n
<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : multiplicity.Finite p n<GOAL>p.maxPowDiv n = (multiplicity p n).get h
<VAR>p : ℕ<GOAL>padicValInt p 0 = 0
<VAR>p : ℕ<GOAL>padicValInt p 1 = 0
<VAR>p n : ℕ<GOAL>padicValInt p ↑n = padicValNat p n
<VAR>p : ℕ<VAR>z : ℤ<VAR>h : ¬↑p ∣ z<GOAL>padicValInt p z = 0
<VAR>p : ℕ<VAR>q : ℚ<GOAL>padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)
<VAR>p : ℕ<VAR>q : ℚ<GOAL>padicValRat p (-q) = padicValRat p q
<VAR>p : ℕ<GOAL>padicValRat p 0 = 0
<VAR>p : ℕ<GOAL>padicValRat p 1 = 0
<VAR>p : ℕ<VAR>z : ℤ<GOAL>padicValRat p ↑z = ↑(padicValInt p z)
<VAR>p n : ℕ<GOAL>padicValRat p ↑n = ↑(padicValNat p n)
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>padicValRat p ↑p = 1
<VAR>p : ℕ<VAR>n : ℕ<GOAL>0 ≤ padicValRat p ↑n
<VAR>p : ℕ<VAR>n : ℕ<GOAL>↑(padicValNat p n) = padicValRat p ↑n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>padicValNat p n = (multiplicity p n).get ⋯
<VAR>p n : ℕ<VAR>hp : p ≠ 1<VAR>hn : 0 < n<GOAL>↑(padicValNat p n) = multiplicity p n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>padicValNat p p = 1
<VAR>p n : ℕ<VAR>Fact (Nat.Prime p)<VAR>hn0 : n ≠ 0<GOAL>p ∣ n ↔ padicValNat p n ≠ 0
<VAR>a b n : ℕ<VAR>ha : Nat.Prime a<VAR>hb : b ≠ 0<GOAL>↑n ≤ multiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList
<VAR>a b n : ℕ<VAR>ha : Nat.Prime a<VAR>hb : b ≠ 0<GOAL>n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<GOAL>padicValRat p q = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>padicValRat p q⁻¹ = -padicValRat p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<GOAL>min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r₁ r₂ : ℚ<VAR>hqr : r₁ + r₂ ≠ 0<VAR>hval₁ : padicValRat p q < padicValRat p r₁<VAR>hval₂ : padicValRat p q < padicValRat p r₂<GOAL>padicValRat p q < padicValRat p (r₁ + r₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>F : ℕ → ℚ<VAR>hF : ∀ i < n, 0 < padicValRat p (F i)<VAR>hn0 : ∑ i ∈ Finset.range n, F i ≠ 0<GOAL>0 < padicValRat p (∑ i ∈ Finset.range n, F i)
<VAR>p j : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>F : ℕ → ℚ<VAR>S : Finset ℕ<VAR>hS : S.Nonempty<VAR>hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)<VAR>hn1 : ∀ (i : ℕ), 0 < F i<GOAL>padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)