ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>x : ℂ<GOAL>⇑(ModularForm.const x) = Function.const ℍ x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>x : ℂ<GOAL>(ModularForm.const x).toSlashInvariantForm = SlashInvariantForm.const x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>n : ℕ<GOAL>(↑n).toSlashInvariantForm = ↑n
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>z : ℤ<GOAL>(↑z).toSlashInvariantForm = ↑z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : CuspForm Γ k<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : CuspForm Γ k<VAR>z : ℍ<GOAL>(f + g) z = f z + g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : CuspForm Γ k<VAR>n : α<GOAL>⇑(n • f) = n • ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : CuspForm Γ k<VAR>n : α<VAR>z : ℍ<GOAL>(n • f) z = n • f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : CuspForm Γ k<GOAL>⇑(-f) = -⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : CuspForm Γ k<VAR>z : ℍ<GOAL>(-f) z = -f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : CuspForm Γ k<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : CuspForm Γ k<VAR>z : ℍ<GOAL>(f - g) z = f z - g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : CuspForm Γ k<VAR>a : ℍ<GOAL>CuspForm.coeHom f a = f a
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>a b : GradedMonoid (ModularForm Γ)<VAR>h : a.fst = b.fst<VAR>h2 : ModularForm.mcast h a.snd = b.snd<GOAL>a = b
<VAR>N : ℕ<VAR>γ : SL(2, ℤ)<VAR>i j : Fin 2<GOAL>↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑(↑γ i j)
<VAR>N : ℕ<VAR>γ : SL(2, ℤ)<GOAL>γ ∈ CongruenceSubgroup.Gamma N ↔ (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
<VAR>N : ℕ<VAR>γ : SL(2, ℤ)<GOAL>γ ∈ CongruenceSubgroup.Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
<VAR>N : ℕ<GOAL>(CongruenceSubgroup.Gamma N).Normal
<VAR>N M : ℤ<VAR>hNM : N ∣ M<GOAL>ModularGroup.T ^ M ∈ CongruenceSubgroup.Gamma N.natAbs
<VAR>N : ℕ<VAR>A : SL(2, ℤ)<GOAL>A ∈ CongruenceSubgroup.Gamma0 N ↔ ↑(↑A 1 0) = 0
<VAR>N : ℕ<VAR>A : ↥(CongruenceSubgroup.Gamma0 N)<GOAL>↑(↑↑A).det = 1
<VAR>N : ℕ<VAR>γ : ↥(CongruenceSubgroup.Gamma0 N)<GOAL>γ ∈ CongruenceSubgroup.Gamma1' N ↔ (CongruenceSubgroup.Gamma0Map N) γ = 1
<VAR>N : ℕ<VAR>A : ↥(CongruenceSubgroup.Gamma0 N)<GOAL>A ∈ CongruenceSubgroup.Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
<VAR>N : ℕ<VAR>A : SL(2, ℤ)<GOAL>A ∈ CongruenceSubgroup.Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
<VAR>N : ℕ<GOAL>CongruenceSubgroup.Gamma1 N ≤ CongruenceSubgroup.Gamma0 N
<VAR>H K : Subgroup SL(2, ℤ)<VAR>h : H ≤ K<VAR>h2 : CongruenceSubgroup.IsCongruenceSubgroup H<GOAL>CongruenceSubgroup.IsCongruenceSubgroup K
<VAR>N : ℕ+<GOAL>CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma ↑N)
<VAR>N : ℕ+<GOAL>CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma1 ↑N)
<VAR>N : ℕ+<GOAL>CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma0 ↑N)
<VAR>N : ℕ<VAR>g : ConjAct SL(2, ℤ)<GOAL>g • CongruenceSubgroup.Gamma N = CongruenceSubgroup.Gamma N
<VAR>g : ConjAct SL(2, ℤ)<VAR>Γ : Subgroup SL(2, ℤ)<VAR>h : CongruenceSubgroup.IsCongruenceSubgroup Γ<GOAL>CongruenceSubgroup.IsCongruenceSubgroup (g • Γ)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>legendreSym p 2 = ZMod.χ₈ ↑p
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>legendreSym p (-2) = ZMod.χ₈' ↑p
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>hpq : p ≠ q<GOAL>legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<GOAL>legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp : p % 4 = 1<VAR>hq : q ≠ 2<GOAL>legendreSym q ↑p = legendreSym p ↑q
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp : p % 4 = 3<VAR>hq : q % 4 = 3<GOAL>legendreSym q ↑p = -legendreSym p ↑q
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp1 : p % 4 = 1<VAR>hq1 : q ≠ 2<GOAL>IsSquare ↑q ↔ IsSquare ↑p
<VAR>p q : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (Nat.Prime q)<VAR>hp3 : p % 4 = 3<VAR>hq3 : q % 4 = 3<VAR>hpq : p ≠ q<GOAL>IsSquare ↑q ↔ ¬IsSquare ↑p
<VAR>x : ℝ<VAR>h : Liouville x<GOAL>Irrational x
<VAR>Z : Type u_1<VAR>N : Type u_2<VAR>R : Type u_3<VAR>PseudoMetricSpace R<VAR>d : N → ℝ<VAR>j : Z → N → R<VAR>f : R → R<VAR>α : R<VAR>ε M : ℝ<VAR>d0 : ∀ (a : N), 1 ≤ d a<VAR>e0 : 0 < ε<VAR>B : ∀ ⦃y : R⦄, y ∈ Metric.closedBall α ε → dist (f α) (f y) ≤ dist α y * M<VAR>L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ Metric.closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))<GOAL>∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : Polynomial ℤ<VAR>f0 : f ≠ 0<VAR>fa : Polynomial.eval α (Polynomial.map (algebraMap ℤ ℝ) f) = 0<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>x : ℝ<VAR>lx : Liouville x<GOAL>Transcendental ℤ x
<VAR>m n : ℕ<GOAL>(m + n)# = m# * ∏ p ∈ Finset.filter Nat.Prime (Finset.Ico (m + 1) (m + n + 1)), p
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>(m + n)# ∣ m# * (m + n).choose m
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>(m + n)# ≤ m# * (m + n).choose m
<VAR>a : ZMod 4<GOAL>ZMod.χ₄ a = match a with | 0 => 0 | 2 => 0 | 1 => 1 | 3 => -1
<VAR>n : ℕ<GOAL>ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
<VAR>n : ℤ<GOAL>ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
<VAR>n : ℤ<GOAL>ZMod.χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
<VAR>n : ℕ<GOAL>ZMod.χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>ZMod.χ₄ ↑n = (-1) ^ (n / 2)
<VAR>n : ℕ<VAR>hn : n % 4 = 1<GOAL>ZMod.χ₄ ↑n = 1
<VAR>n : ℕ<VAR>hn : n % 4 = 3<GOAL>ZMod.χ₄ ↑n = -1
<VAR>n : ℤ<VAR>hn : n % 4 = 1<GOAL>ZMod.χ₄ ↑n = 1
<VAR>n : ℤ<VAR>hn : n % 4 = 3<GOAL>ZMod.χ₄ ↑n = -1
<VAR>n : ℕ<VAR>hn : n % 4 = 1<GOAL>(-1) ^ (n / 2) = 1
<VAR>n : ℕ<VAR>hn : n % 4 = 3<GOAL>(-1) ^ (n / 2) = -1
<VAR>a : ZMod 8<GOAL>ZMod.χ₈ a = match a with | 0 => 0 | 2 => 0 | 4 => 0 | 6 => 0 | 1 => 1 | 7 => 1 | 3 => -1 | 5 => -1
<VAR>n : ℕ<GOAL>ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
<VAR>n : ℤ<GOAL>ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
<VAR>n : ℤ<GOAL>ZMod.χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
<VAR>n : ℕ<GOAL>ZMod.χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
<VAR>a : ZMod 8<GOAL>ZMod.χ₈' a = match a with | 0 => 0 | 2 => 0 | 4 => 0 | 6 => 0 | 1 => 1 | 3 => 1 | 5 => -1 | 7 => -1
<VAR>n : ℤ<GOAL>ZMod.χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
<VAR>n : ℕ<GOAL>ZMod.χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
<VAR>a : ZMod 8<GOAL>ZMod.χ₈' a = ZMod.χ₄ a.cast * ZMod.χ₈ a
<VAR>a : ℤ<GOAL>ZMod.χ₈' ↑a = ZMod.χ₄ ↑a * ZMod.χ₈ ↑a
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<GOAL>quadraticCharFun F a = 0 ↔ a = 0
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<GOAL>quadraticCharFun F 0 = 0
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<GOAL>quadraticCharFun F 1 = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F = 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>quadraticCharFun F a = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a b : F<GOAL>quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<GOAL>(quadraticChar F) a = quadraticCharFun F a
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<GOAL>(quadraticChar F) a = 0 ↔ a = 0
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<GOAL>(quadraticChar F) 0 = 0
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = 1 ↔ IsSquare a
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) (a ^ 2) = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a ^ 2 = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = -1 ↔ ¬(quadraticChar F) a = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>a : F<GOAL>(quadraticChar F) a = -1 ↔ ¬IsSquare a
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>∃ a, (quadraticChar F) a = -1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>∃ a, (quadraticChar F) ↑a = -1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F = 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>(quadraticChar F) a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<GOAL>↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<GOAL>(quadraticChar F).IsQuadratic
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>quadraticChar F ≠ 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F).IsNontrivial
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : F<GOAL>↑{x | x ^ 2 = a}.toFinset.card = (quadraticChar F) a + 1
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>∑ a : F, (quadraticChar F) a = 0
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F) (-1) = ZMod.χ₄ ↑(Fintype.card F)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<GOAL>IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
<VAR>c d : ℝ<VAR>hcd : c ≤ d<GOAL>(fun t => rexp (-d * t)) =O[Filter.atTop] fun t => rexp (-c * t)
<GOAL>(fun t => (1 - rexp (-π * t))⁻¹) =O[Filter.atTop] fun x => 1
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>‖HurwitzKernelBounds.f_nat k a t n‖ ≤ HurwitzKernelBounds.g_nat k a t n
<VAR>k : ℕ<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>Summable (HurwitzKernelBounds.f_nat k a t)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖HurwitzKernelBounds.F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖HurwitzKernelBounds.F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<GOAL>∃ p, 0 < p ∧ (fun t => HurwitzKernelBounds.F_nat 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖HurwitzKernelBounds.F_nat 1 a t‖ ≤ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<GOAL>∃ p, 0 < p ∧ HurwitzKernelBounds.F_nat 1 a =O[Filter.atTop] fun t => rexp (-p * t)
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>n : ℕ<GOAL>HurwitzKernelBounds.f_int k a t (Int.ofNat n) = HurwitzKernelBounds.f_nat k a t n
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ≤ 1<VAR>t : ℝ<VAR>n : ℕ<GOAL>HurwitzKernelBounds.f_int k a t (Int.negSucc n) = HurwitzKernelBounds.f_nat k (1 - a) t n
<VAR>k : ℕ<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>Summable (HurwitzKernelBounds.f_int k a t)
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ∈ Set.Icc 0 1<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HurwitzKernelBounds.F_int k (↑a) t = HurwitzKernelBounds.F_nat k a t + HurwitzKernelBounds.F_nat k (1 - a) t
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun t => HurwitzKernelBounds.F_int 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun t => rexp (-p * t)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ HurwitzKernelBounds.F_int 1 a =O[Filter.atTop] fun t => rexp (-p * t)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F) 2 = ZMod.χ₈ ↑(Fintype.card F)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<GOAL>IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>(quadraticChar F) (-2) = ZMod.χ₈' ↑(Fintype.card F)
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<GOAL>IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>F' : Type u_2<VAR>Field F'<VAR>Fintype F'<VAR>DecidableEq F'<VAR>hF' : ringChar F' ≠ 2<VAR>h : ringChar F' ≠ ringChar F<GOAL>(quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp₁ : p ≠ 2<VAR>hp₂ : ringChar F ≠ p<GOAL>(quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))
<VAR>F : Type u_1<VAR>Field F<VAR>Fintype F<VAR>hF : ringChar F ≠ 2<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1
<VAR>R : Type u<VAR>CommRing R<VAR>R' : Type v<VAR>CommMonoid R'<VAR>φ : AddChar R R'<VAR>a : R<VAR>h : 0 < ringChar R<GOAL>⋯.unit ∈ rootsOfUnity (ringChar R).toPNat' R'
<VAR>R : Type u<VAR>CommRing R<VAR>R' : Type v<VAR>CommMonoid R'<VAR>R'' : Type u_1<VAR>CommMonoid R''<VAR>φ : AddChar R R'<VAR>f : R' →* R''<VAR>hφ : φ.IsPrimitive<VAR>hf : Function.Injective ⇑f<GOAL>(f.compAddChar φ).IsPrimitive
<VAR>R : Type u<VAR>CommRing R<VAR>R' : Type v<VAR>CommMonoid R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>Function.Injective ψ.mulShift
<VAR>R' : Type v<VAR>CommMonoid R'<VAR>F : Type u<VAR>Field F<VAR>ψ : AddChar F R'<VAR>hψ : ψ ≠ 1<GOAL>ψ.IsPrimitive
<VAR>R : Type u<VAR>CommRing R<VAR>R' : Type v<VAR>CommMonoid R'<VAR>Finite R<VAR>e : AddChar R R'<VAR>r : R<VAR>hr : ¬IsUnit r<GOAL>¬(e.mulShift r).IsPrimitive
<VAR>R : Type u<VAR>CommRing R<VAR>R' : Type v<VAR>Field R'<VAR>self : AddChar.PrimitiveAddChar R R'<GOAL>self.char.IsPrimitive
<VAR>N : ℕ<VAR>NeZero N<VAR>R : Type u_1<VAR>CommRing R<VAR>e : AddChar (ZMod N) R<VAR>he : ¬e.IsPrimitive<GOAL>∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>NeZero n<VAR>ζ : C<VAR>hζ : ζ ^ n = 1<VAR>a : ZMod n<GOAL>(AddChar.zmodChar n hζ) a = ζ ^ a.val
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>NeZero n<VAR>ζ : C<VAR>hζ : ζ ^ n = 1<VAR>a : ℕ<GOAL>(AddChar.zmodChar n hζ) ↑a = ζ ^ a
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>NeZero n<VAR>ψ : AddChar (ZMod n) C<GOAL>ψ ≠ 1 ↔ ψ 1 ≠ 1
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>NeZero n<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ψ.IsPrimitive<VAR>a : ZMod n<GOAL>ψ a = 1 ↔ a = 0
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0<GOAL>ψ.IsPrimitive
<VAR>C : Type v<VAR>CommMonoid C<VAR>n : ℕ<VAR>NeZero n<VAR>ζ : C<VAR>h : IsPrimitiveRoot ζ n<GOAL>(AddChar.zmodChar n ⋯).IsPrimitive
<VAR>R : Type u_1<VAR>AddGroup R<VAR>Fintype R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>IsDomain R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ ≠ 1<GOAL>∑ a : R, ψ a = 0
<VAR>R : Type u_1<VAR>AddGroup R<VAR>Fintype R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>ψ : AddChar R R'<VAR>hψ : ψ = 1<GOAL>∑ a : R, ψ a = ↑(Fintype.card R)
<VAR>R : Type u_1<VAR>CommRing R<VAR>Fintype R<VAR>DecidableEq R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>IsDomain R'<VAR>ψ : AddChar R R'<VAR>b : R<VAR>hψ : ψ.IsPrimitive<GOAL>∑ x : R, ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)
<VAR>R : Type u_1<VAR>CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<GOAL>(↑(starRingEnd ℂ)).compAddChar φ = φ⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<GOAL>(starRingEnd ℂ) (φ a) = φ⁻¹ a
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<GOAL>ringChar ℂ ≠ ringChar F
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<GOAL>(AddChar.FiniteField.primitiveChar_to_Complex F).IsPrimitive
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<GOAL>∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
<VAR>p q x : ℝ<VAR>h : LiouvilleWith p x<VAR>hle : q ≤ p<GOAL>LiouvilleWith q x
<VAR>p q x : ℝ<VAR>h : LiouvilleWith p x<VAR>hlt : q < p<GOAL>∃ᶠ (n : ℕ) in Filter.atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p x : ℝ<VAR>r : ℚ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (x * ↑r)
<VAR>p x : ℝ<VAR>r : ℚ<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (x * ↑r) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>r : ℚ<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>r : ℚ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (↑r * x)
<VAR>p x : ℝ<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>m : ℤ<VAR>h : LiouvilleWith p x<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (x * ↑m)
<VAR>p x : ℝ<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>m : ℤ<VAR>h : LiouvilleWith p x<VAR>hm : m ≠ 0<GOAL>LiouvilleWith p (↑m * x)
<VAR>p x : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (x * ↑n)
<VAR>p x : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (↑n * x)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<GOAL>LiouvilleWith p (x + ↑r)
<VAR>p x : ℝ<VAR>r : ℚ<GOAL>LiouvilleWith p (x + ↑r) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>r : ℚ<GOAL>LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<GOAL>LiouvilleWith p (↑r + x)
<VAR>p x : ℝ<VAR>m : ℤ<GOAL>LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>m : ℤ<GOAL>LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>n : ℕ<GOAL>LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>m : ℤ<GOAL>LiouvilleWith p (x + ↑m)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>m : ℤ<GOAL>LiouvilleWith p (↑m + x)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>n : ℕ<GOAL>LiouvilleWith p (x + ↑n)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n + x)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<GOAL>LiouvilleWith p (-x)
<VAR>p x : ℝ<GOAL>LiouvilleWith p (-x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>r : ℚ<GOAL>LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<GOAL>LiouvilleWith p (x - ↑r)
<VAR>p x : ℝ<VAR>m : ℤ<GOAL>LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>m : ℤ<GOAL>LiouvilleWith p (x - ↑m)
<VAR>p x : ℝ<VAR>n : ℕ<GOAL>LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>n : ℕ<GOAL>LiouvilleWith p (x - ↑n)
<VAR>p x : ℝ<VAR>r : ℚ<GOAL>LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<GOAL>LiouvilleWith p (↑r - x)
<VAR>p x : ℝ<VAR>m : ℤ<GOAL>LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>m : ℤ<GOAL>LiouvilleWith p (↑m - x)
<VAR>p x : ℝ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n - x)
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>hp : 1 < p<VAR>m : ℤ<GOAL>x ≠ ↑m
<VAR>p x : ℝ<VAR>h : LiouvilleWith p x<VAR>hp : 1 < p<GOAL>Irrational x
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>n : ℕ<GOAL>∃ᶠ (b : ℕ) in Filter.atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
<VAR>n : ℕ<GOAL>ArithmeticFunction.log n = Real.log ↑n
<VAR>n : ℕ<GOAL>ArithmeticFunction.vonMangoldt n = if IsPrimePow n then Real.log ↑n.minFac else 0
<GOAL>ArithmeticFunction.vonMangoldt 1 = 0
<VAR>n : ℕ<GOAL>0 ≤ ArithmeticFunction.vonMangoldt n
<VAR>n k : ℕ<VAR>hk : k ≠ 0<GOAL>ArithmeticFunction.vonMangoldt (n ^ k) = ArithmeticFunction.vonMangoldt n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>ArithmeticFunction.vonMangoldt p = Real.log ↑p
<VAR>n : ℕ<GOAL>ArithmeticFunction.vonMangoldt n ≠ 0 ↔ IsPrimePow n
<VAR>n : ℕ<GOAL>0 < ArithmeticFunction.vonMangoldt n ↔ IsPrimePow n
<VAR>n : ℕ<GOAL>ArithmeticFunction.vonMangoldt n = 0 ↔ ¬IsPrimePow n
<VAR>n : ℕ<GOAL>∑ i ∈ n.divisors, ArithmeticFunction.vonMangoldt i = Real.log ↑n
<GOAL>ArithmeticFunction.vonMangoldt * ↑ArithmeticFunction.zeta = ArithmeticFunction.log
<GOAL>↑ArithmeticFunction.zeta * ArithmeticFunction.vonMangoldt = ArithmeticFunction.log
<GOAL>ArithmeticFunction.log * ↑ArithmeticFunction.moebius = ArithmeticFunction.vonMangoldt
<GOAL>↑ArithmeticFunction.moebius * ArithmeticFunction.log = ArithmeticFunction.vonMangoldt
<VAR>n : ℕ<GOAL>∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.log d = -ArithmeticFunction.vonMangoldt n
<VAR>n : ℕ<GOAL>ArithmeticFunction.vonMangoldt n ≤ Real.log ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c d x y z w : R<GOAL>(a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 + (a * w + b * z - c * y + d * x) ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
<VAR>m x y : ℤ<VAR>h : 2 * m = x ^ 2 + y ^ 2<GOAL>m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>n : ℕ<GOAL>(Nat.nth Nat.Prime n).primeCounting' = n
<VAR>n : ℕ<GOAL>Nat.Prime (Nat.nth Nat.Prime n)
<VAR>n : ℕ<GOAL>n.primesBelow.card = n.primeCounting'
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>(k + n).primeCounting' ≤ k.primeCounting' + a.totient * (n / a + 1)
<VAR>n : ℕ<GOAL>n + 2 ≤ Nat.nth Nat.Prime n
<VAR>k n : ℕ<GOAL>n ∈ k.primesBelow ↔ n < k ∧ Nat.Prime n
<VAR>p n : ℕ<VAR>h : p ∈ n.primesBelow<GOAL>Nat.Prime p
<VAR>p n : ℕ<VAR>h : p ∈ n.primesBelow<GOAL>p < n
<VAR>n : ℕ<GOAL>n.succ.primesBelow = if Nat.Prime n then insert n n.primesBelow else n.primesBelow
<VAR>n : ℕ<GOAL>n ∉ n.primesBelow
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
<VAR>s : Finset ℕ<VAR>m k : ℕ<VAR>h : m ∈ Nat.factoredNumbers s<VAR>h' : k ∣ m<GOAL>k ∈ Nat.factoredNumbers s
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ Nat.factoredNumbers s ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m : ℕ<VAR>h : m ∈ Nat.factoredNumbers s<GOAL>m ≠ 0
<VAR>s : Finset ℕ<VAR>m : ℕ<VAR>hm : m ∈ Nat.factoredNumbers s<GOAL>m.primeFactors ⊆ s
<VAR>s : Finset ℕ<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>hp : m.primeFactors ⊆ s<GOAL>m ∈ Nat.factoredNumbers s
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ m.primeFactors ⊆ s
<VAR>s : Finset ℕ<VAR>m n : ℕ<VAR>hm : m ∈ Nat.factoredNumbers s<VAR>hn : n ∈ Nat.factoredNumbers s<GOAL>m * n ∈ Nat.factoredNumbers s
<VAR>s : Finset ℕ<VAR>n : ℕ<GOAL>(List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ∈ Nat.factoredNumbers s
<VAR>s : Finset ℕ<VAR>N : ℕ<VAR>hN : ¬Nat.Prime N<GOAL>Nat.factoredNumbers (insert N s) = Nat.factoredNumbers s
<VAR>s t : Finset ℕ<VAR>hst : s ≤ t<GOAL>Nat.factoredNumbers s ⊆ Nat.factoredNumbers t
<VAR>N : ℕ<VAR>s : Finset ℕ<VAR>h : N.primesBelow ≤ s<GOAL>(Nat.factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>e : ℕ<VAR>hn : n ∈ Nat.factoredNumbers s<GOAL>p ^ e * n ∈ Nat.factoredNumbers (insert p s)
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hs : p ∉ s<VAR>hn : n ∈ Nat.factoredNumbers s<GOAL>p.Coprime n