ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>LowerSet.Iic x = LowerSet.Iic x.1 ×ˢ LowerSet.Iic x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>LowerSet.Iic a ×ˢ LowerSet.Iic b = LowerSet.Iic (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<GOAL>s ×ˢ ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>t : LowerSet β<GOAL>⊥ ×ˢ t = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>⊤ ×ˢ ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t : LowerSet β<GOAL>(s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t : LowerSet β<GOAL>(s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t : LowerSet β<GOAL>s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s₁ s₂ : LowerSet α<GOAL>s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s₁ s₂ : LowerSet α<GOAL>s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>t : LowerSet β<GOAL>s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : LowerSet α<VAR>t₁ t₂ : LowerSet β<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>t : Set β<GOAL>upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>t : Set β<GOAL>lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (CongruenceSubgroup.Gamma N) k<VAR>z : ℍ<GOAL>f (↑N * ↑n +ᵥ z) = f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (CongruenceSubgroup.Gamma N) k<VAR>z : ℍ<GOAL>f (ModularGroup.T ^ (↑N * n) • z) = f z
<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (jacobiTheta ∘ UpperHalfPlane.coe)
<GOAL>{x | Liouville x} = ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
<GOAL>{x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n)
<VAR>k : ℕ<GOAL>1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p
<GOAL>¬Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
<VAR>r : ℝ<GOAL>(Summable fun p => ↑↑p ^ r) ↔ r < -1
<VAR>N : ℕ<VAR>NeZero N<VAR>R : Type u_1<VAR>CommRing R<VAR>e : AddChar (ZMod N) R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>u : (ZMod N)ˣ<VAR>hu : (ZMod.unitsMap hd) u = 1<GOAL>χ ↑u * gaussSum χ e = gaussSum χ e
<VAR>N : ℕ<VAR>NeZero N<VAR>R : Type u_1<VAR>CommRing R<VAR>e : AddChar (ZMod N) R<VAR>IsDomain R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>h_ne : gaussSum χ e ≠ 0<GOAL>χ.FactorsThrough d
<VAR>N : ℕ<VAR>NeZero N<VAR>R : Type u_1<VAR>CommRing R<VAR>e : AddChar (ZMod N) R<VAR>IsDomain R<VAR>χ : DirichletCharacter R N<VAR>hχ : χ.IsPrimitive<VAR>he : ¬e.IsPrimitive<GOAL>gaussSum χ e = 0
<VAR>N : ℕ<VAR>NeZero N<VAR>R : Type u_1<VAR>CommRing R<VAR>e : AddChar (ZMod N) R<VAR>IsDomain R<VAR>χ : DirichletCharacter R N<VAR>hχ : χ.IsPrimitive<VAR>a : ZMod N<GOAL>gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e
<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>self : SlashInvariantForm Γ k<VAR>γ : ↥Γ<GOAL>self.toFun ∣[k] γ = self.toFun
<VAR>F : Type u_1<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>FunLike F ℍ ℂ<VAR>self : SlashInvariantFormClass F Γ k<VAR>f : F<VAR>γ : ↥Γ<GOAL>⇑f ∣[k] γ = ⇑f
<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>f : SlashInvariantForm Γ k<GOAL>f.toFun = ⇑f
<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>f : ℍ → ℂ<VAR>hf : ∀ (γ : ↥Γ), f ∣[k] γ = f<GOAL>⇑{ toFun := f, slash_action_eq' := hf } = f
<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>f g : SlashInvariantForm Γ k<VAR>h : ∀ (x : ℍ), f x = g x<GOAL>f = g
<VAR>F : Type u_1<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>FunLike F ℍ ℂ<VAR>SlashInvariantFormClass F Γ k<VAR>f : F<VAR>γ : ↥Γ<GOAL>⇑f ∣[k] γ = ⇑f
<VAR>F : Type u_1<VAR>FunLike F ℍ ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>SlashInvariantFormClass F Γ k<VAR>f : F<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
<VAR>F : Type u_1<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>FunLike F ℍ ℂ<VAR>SlashInvariantFormClass F Γ k<VAR>f : F<GOAL>⇑{ toFun := ⇑f, slash_action_eq' := ⋯ } = ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : SlashInvariantForm Γ k<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : SlashInvariantForm Γ k<VAR>z : ℍ<GOAL>(f + g) z = f z + g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<GOAL>⇑0 = 0
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : SlashInvariantForm Γ k<VAR>n : α<GOAL>⇑(n • f) = n • ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : SlashInvariantForm Γ k<VAR>n : α<VAR>z : ℍ<GOAL>(n • f) z = n • f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : SlashInvariantForm Γ k<GOAL>⇑(-f) = -⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : SlashInvariantForm Γ k<VAR>z : ℍ<GOAL>(-f) z = -f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : SlashInvariantForm Γ k<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : SlashInvariantForm Γ k<VAR>z : ℍ<GOAL>(f - g) z = f z - g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<GOAL>Function.Injective ⇑SlashInvariantForm.coeHom
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>x : ℂ<GOAL>⇑(SlashInvariantForm.const x) = Function.const ℍ x
<VAR>Γ : Subgroup SL(2, ℤ)<GOAL>⇑1 = 1
<VAR>k₁ k₂ : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : SlashInvariantForm Γ k₁<VAR>g : SlashInvariantForm Γ k₂<GOAL>⇑(f.mul g) = ⇑f * ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>n : ℕ<GOAL>⇑↑n = ↑n
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>z : ℤ<GOAL>⇑↑z = ↑z
<VAR>m : ℝ<VAR>hm : 1 < m<GOAL>Summable fun i => 1 / m ^ i !
<VAR>m : ℝ<VAR>hm : 1 < m<VAR>k : ℕ<GOAL>0 < LiouvilleNumber.remainder m k
<VAR>m : ℝ<VAR>n : ℕ<GOAL>LiouvilleNumber.partialSum m (n + 1) = LiouvilleNumber.partialSum m n + 1 / m ^ (n + 1)!
<VAR>m : ℝ<VAR>hm : 1 < m<VAR>k : ℕ<GOAL>LiouvilleNumber.partialSum m k + LiouvilleNumber.remainder m k = liouvilleNumber m
<VAR>n : ℕ<VAR>m : ℝ<VAR>m1 : 1 < m<GOAL>LiouvilleNumber.remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>(1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 1 / (m ^ n !) ^ n
<VAR>n : ℕ<VAR>m : ℝ<VAR>m2 : 2 ≤ m<GOAL>LiouvilleNumber.remainder m n < 1 / (m ^ n !) ^ n
<VAR>m : ℕ<VAR>hm : 0 < m<VAR>k : ℕ<GOAL>∃ p, LiouvilleNumber.partialSum (↑m) k = ↑p / ↑(m ^ k !)
<VAR>m : ℕ<VAR>hm : 2 ≤ m<GOAL>Liouville (liouvilleNumber ↑m)
<VAR>m : ℕ<VAR>hm : 2 ≤ m<GOAL>Transcendental ℤ (liouvilleNumber ↑m)
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<GOAL>Summable fun x => ‖EisensteinSeries.eisSummand k x z‖
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>z : ℍ<GOAL>Complex.abs (eisensteinSeries a k z) ≤ ∑' (x : Fin 2 → ℤ), Complex.abs (EisensteinSeries.eisSummand k x z)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<GOAL>UpperHalfPlane.IsBoundedAtImInfty ((EisensteinSeries.eisensteinSeries_SIF a k).toFun ∣[k] A)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>a : ZMod n<VAR>ha : IsUnit a<GOAL>χ a = ↑((MulChar.toUnitHom χ) ha.unit)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ ψ : DirichletCharacter R n<GOAL>MulChar.toUnitHom χ = MulChar.toUnitHom ψ ↔ χ = ψ
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>x : ZMod n<GOAL>χ (↑n - x) = χ (-x)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>hm : n ∣ m<GOAL>(DirichletCharacter.changeLevel hm) χ = MulChar.ofUnitHom ((MulChar.toUnitHom χ).comp (ZMod.unitsMap hm))
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>hm : n ∣ m<GOAL>MulChar.toUnitHom ((DirichletCharacter.changeLevel hm) χ) = (MulChar.toUnitHom χ).comp (ZMod.unitsMap hm)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n m : ℕ<VAR>NeZero m<VAR>hm : n ∣ m<GOAL>Function.Injective ⇑(DirichletCharacter.changeLevel hm)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n m : ℕ<VAR>χ : DirichletCharacter R n<VAR>hm : n ∣ m<VAR>NeZero m<GOAL>(DirichletCharacter.changeLevel hm) χ = 1 ↔ χ = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>(DirichletCharacter.changeLevel ⋯) χ = χ
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) χ) = MulChar.toUnitHom χ
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(DirichletCharacter.changeLevel ⋯) χ = (DirichletCharacter.changeLevel hd) ((DirichletCharacter.changeLevel hm) χ)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>hm : n ∣ m<VAR>a : (ZMod m)ˣ<GOAL>((DirichletCharacter.changeLevel hm) χ) ↑a = χ (↑a).cast
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>hm : n ∣ m<GOAL>((DirichletCharacter.changeLevel hm) χ).FactorsThrough n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>h : χ.FactorsThrough d<GOAL>d ∣ n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>h : χ.FactorsThrough d<GOAL>χ = (DirichletCharacter.changeLevel ⋯) h.χ₀
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>NeZero n<VAR>h : χ.FactorsThrough d<GOAL>∃! χ', χ = (DirichletCharacter.changeLevel ⋯) χ'
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.FactorsThrough n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>NeZero n<VAR>hd : d ∣ n<GOAL>χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>χ : DirichletCharacter R 1<GOAL>χ = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n = 1<GOAL>χ = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n d : ℕ<VAR>h : d ∣ n<GOAL>(DirichletCharacter.changeLevel h) 1 = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.FactorsThrough 1 ↔ χ = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>x : ℕ<GOAL>x ∈ χ.conductorSet ↔ χ.FactorsThrough x
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>n ∈ χ.conductorSet
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>x : ℕ<VAR>hx : x ∈ χ.conductorSet<GOAL>x ∣ n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.conductor ∈ χ.conductorSet
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.conductor ∣ n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.FactorsThrough χ.conductor
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n ≠ 0<GOAL>χ.conductor ≠ 0
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>DirichletCharacter.conductor 1 = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n ≠ 0<GOAL>χ = 1 ↔ χ.conductor = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.conductor = 0 ↔ n = 0
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>d : ℕ<VAR>hd : d ∈ χ.conductorSet<GOAL>χ.conductor ≤ (Classical.choose ⋯).conductor
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.IsPrimitive ↔ χ.conductor = n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<GOAL>DirichletCharacter.IsPrimitive 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<GOAL>DirichletCharacter.conductor 1 ∣ n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.primitiveCharacter.IsPrimitive
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>DirichletCharacter.primitiveCharacter 1 = 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n m : ℕ<VAR>χ : DirichletCharacter R n<VAR>ψ : DirichletCharacter R m<GOAL>χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>ψ : DirichletCharacter R m<GOAL>(χ.primitive_mul ψ).IsPrimitive
<VAR>S : Type<VAR>CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>NoZeroDivisors S<GOAL>ψ.Even ∨ ψ.Odd
<VAR>S : Type<VAR>CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Odd<GOAL>(MulChar.toUnitHom ψ) (-1) = -1
<VAR>S : Type<VAR>CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>hψ : ψ.Even<GOAL>(MulChar.toUnitHom ψ) (-1) = 1
<VAR>S : Type<VAR>CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ.Odd<GOAL>ψ (-x) = -ψ x
<VAR>S : Type<VAR>CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ.Even<GOAL>ψ (-x) = ψ x
<VAR>N : ℕ<GOAL>Pairwise (Disjoint on EisensteinSeries.gammaSet N)
<VAR>a a' : Fin 2 → ZMod 1<GOAL>EisensteinSeries.gammaSet 1 a = EisensteinSeries.gammaSet 1 a'
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ EisensteinSeries.gammaSet N a<VAR>γ : SL(2, ℤ)<GOAL>v ᵥ* ↑γ ∈ EisensteinSeries.gammaSet N (a ᵥ* ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))
<VAR>k : ℤ<VAR>i : Fin 2 → ℤ<VAR>A : SL(2, ℤ)<VAR>z : ℍ<GOAL>EisensteinSeries.eisSummand k i (A • z) = UpperHalfPlane.denom (↑A) z ^ k * EisensteinSeries.eisSummand k (i ᵥ* ↑A) z
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>γ : SL(2, ℤ)<GOAL>eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>z : ℍ<GOAL>(EisensteinSeries.eisensteinSeries_SIF a k) z = eisensteinSeries a k z
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<GOAL>DifferentiableOn ℂ (EisensteinSeries.eisSummand k a ∘ ↑UpperHalfPlane.ofComplex) {z | 0 < z.im}
<VAR>k : ℤ<VAR>N : ℕ<VAR>hk : 3 ≤ k<VAR>a : Fin 2 → ZMod N<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑(EisensteinSeries.eisensteinSeries_SIF a k)
<GOAL>{x | ∃ p > 2, LiouvilleWith p x} ⊆ ⋃ m, (fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
<GOAL>MeasureTheory.volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0
<GOAL>∀ᵐ (x : ℝ), ¬Liouville x
<GOAL>MeasureTheory.volume {x | Liouville x} = 0
<GOAL>Disjoint (residual ℝ) (MeasureTheory.ae MeasureTheory.volume)
<VAR>τ : ℂ<GOAL>jacobiTheta τ = jacobiTheta₂ 0 τ
<VAR>τ : ℂ<GOAL>jacobiTheta (2 + τ) = jacobiTheta τ
<VAR>τ : ℍ<GOAL>jacobiTheta ↑(ModularGroup.S • τ) = (-Complex.I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>n : ℤ<GOAL>‖cexp (↑π * Complex.I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasSum (fun n => cexp (↑π * Complex.I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), cexp (↑π * Complex.I * (↑n + 1) ^ 2 * τ)
<GOAL>(fun τ => jacobiTheta τ - 1) =O[Filter.comap Complex.im Filter.atTop] fun τ => rexp (-π * τ.im)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>ContinuousAt jacobiTheta τ
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : (ZMod p)ˣ<GOAL>(∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>IsSquare a ↔ a ^ (p / 2) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>↑(legendreSym p a) = ↑a ^ (p / 2)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>legendreSym p a = 1 ∨ legendreSym p a = -1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>legendreSym p a = -1 ↔ ¬legendreSym p a = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = 0 ↔ ↑a = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>legendreSym p 0 = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>legendreSym p 1 = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a b : ℤ<GOAL>legendreSym p (a * b) = legendreSym p a * legendreSym p b
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>(legendreSym.hom p) a = legendreSym p a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>legendreSym p a ^ 2 = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<GOAL>legendreSym p (a ^ 2) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = legendreSym p (a % ↑p)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p a = 1 ↔ IsSquare ↑a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p ↑a = 1 ↔ IsSquare ↑a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = -1 ↔ ¬IsSquare ↑a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>a : ℤ<GOAL>↑{x | x ^ 2 = ↑a}.toFinset.card = legendreSym p a + 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<GOAL>legendreSym p a = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : ↑a ≠ 0<VAR>x y : ZMod p<VAR>hx : x ≠ 0<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<GOAL>legendreSym p a = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<GOAL>x = 0 ∧ y = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x ^ 2 - a * y ^ 2<GOAL>↑p ∣ x ∧ ↑p ∣ y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>legendreSym p (-1) = ZMod.χ₄ ↑p
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>IsSquare (-1) ↔ p % 4 ≠ 3
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>y : ZMod p<VAR>hy : y ^ 2 = -1<GOAL>p % 4 ≠ 3
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : x ^ 2 = -y ^ 2<GOAL>p % 4 ≠ 3
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ZMod p<VAR>hx : x ≠ 0<VAR>hxy : x ^ 2 = -y ^ 2<GOAL>p % 4 ≠ 3
<VAR>x : Fin 2 → ℤ<GOAL>‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)
<VAR>z : ℍ<GOAL>EisensteinSeries.r1 z = 1 / ((z.re / z.im) ^ 2 + 1)
<VAR>z : ℍ<GOAL>0 < EisensteinSeries.r1 z
<VAR>z : ℍ<VAR>c : ℝ<VAR>d : ℝ<VAR>hd : 1 ≤ d ^ 2<GOAL>EisensteinSeries.r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
<VAR>z : ℍ<GOAL>0 < EisensteinSeries.r z
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ UpperHalfPlane.verticalStrip A B<GOAL>EisensteinSeries.r ⟨{ re := A, im := B }, h⟩ ≤ EisensteinSeries.r z
<VAR>z : ℍ<VAR>c : ℝ<VAR>d : ℝ<VAR>hc : 1 ≤ c ^ 2<GOAL>EisensteinSeries.r z ≤ Complex.abs (↑c * ↑z + ↑d)
<VAR>z : ℍ<VAR>c : ℝ<VAR>d : ℝ<VAR>hd : 1 ≤ d ^ 2<GOAL>EisensteinSeries.r z ≤ Complex.abs (↑c * ↑z + ↑d)
<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<GOAL>1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<GOAL>EisensteinSeries.r z * ‖x‖ ≤ Complex.abs (↑(x 0) * ↑z + ↑(x 1))
<VAR>z : ℍ<VAR>k : ℝ<VAR>hk : 0 ≤ k<VAR>x : Fin 2 → ℤ<GOAL>Complex.abs (↑(x 0) * ↑z + ↑(x 1)) ^ (-k) ≤ EisensteinSeries.r z ^ (-k) * ‖x‖ ^ (-k)
<VAR>z : ℍ<VAR>k : ℝ<VAR>hk : 0 ≤ k<VAR>x : Fin 2 → ℤ<VAR>A B : ℝ<VAR>hB : 0 < B<VAR>hz : z ∈ UpperHalfPlane.verticalStrip A B<GOAL>Complex.abs (↑(x 0) * ↑z + ↑(x 1)) ^ (-k) ≤ EisensteinSeries.r ⟨{ re := A, im := B }, hB⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>k : ℝ<VAR>hk : 2 < k<GOAL>Summable fun x => ‖x‖ ^ (-k)
<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<GOAL>TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, EisensteinSeries.eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop
<VAR>k : ℤ<VAR>N : ℕ<VAR>hk : 3 ≤ k<VAR>a : Fin 2 → ZMod N<GOAL>TendstoLocallyUniformlyOn (fun s => (fun z => ∑ x ∈ s, EisensteinSeries.eisSummand k (↑x) z) ∘ ↑UpperHalfPlane.ofComplex) ((EisensteinSeries.eisensteinSeries_SIF a k).toFun ∘ ↑UpperHalfPlane.ofComplex) Filter.atTop {z | 0 < z.im}
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>self : ModularForm Γ k<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑self.toSlashInvariantForm
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>self : ModularForm Γ k<VAR>A : SL(2, ℤ)<GOAL>UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>self : CuspForm Γ k<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑self.toSlashInvariantForm
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>self : CuspForm Γ k<VAR>A : SL(2, ℤ)<GOAL>UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)
<VAR>F : Type u_2<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>FunLike F ℍ ℂ<VAR>self : ModularFormClass F Γ k<VAR>f : F<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑f
<VAR>F : Type u_2<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>FunLike F ℍ ℂ<VAR>self : ModularFormClass F Γ k<VAR>f : F<VAR>A : SL(2, ℤ)<GOAL>UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑f)
<VAR>F : Type u_2<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>FunLike F ℍ ℂ<VAR>self : CuspFormClass F Γ k<VAR>f : F<VAR>A : SL(2, ℤ)<GOAL>UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ⇑f)
<VAR>F : Type u_2<VAR>Γ : outParam (Subgroup SL(2, ℤ))<VAR>k : outParam ℤ<VAR>FunLike F ℍ ℂ<VAR>self : CuspFormClass F Γ k<VAR>f : F<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ModularForm Γ k<GOAL>f.toFun = ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ModularForm Γ k<GOAL>⇑f.toSlashInvariantForm = ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : CuspForm Γ k<GOAL>f.toFun = ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : CuspForm Γ k<GOAL>⇑f.toSlashInvariantForm = ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : ModularForm Γ k<VAR>h : ∀ (x : ℍ), f x = g x<GOAL>f = g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : CuspForm Γ k<VAR>h : ∀ (x : ℍ), f x = g x<GOAL>f = g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : ModularForm Γ k<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : ModularForm Γ k<VAR>z : ℍ<GOAL>(f + g) z = f z + g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>z : ℍ<GOAL>0 z = 0
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : ModularForm Γ k<VAR>n : α<GOAL>⇑(n • f) = n • ⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>α : Type u_2<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>f : ModularForm Γ k<VAR>n : α<VAR>z : ℍ<GOAL>(n • f) z = n • f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ModularForm Γ k<GOAL>⇑(-f) = -⇑f
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ModularForm Γ k<VAR>z : ℍ<GOAL>(-f) z = -f z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : ModularForm Γ k<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f g : ModularForm Γ k<VAR>z : ℍ<GOAL>(f - g) z = f z - g z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ModularForm Γ k<VAR>a : ℍ<GOAL>ModularForm.coeHom f a = f a
<VAR>k_1 k_2 : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ModularForm Γ k_1<VAR>g : ModularForm Γ k_2<GOAL>⇑(f.mul g) = ⇑f * ⇑g