ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
<VAR>a b : ℕ<VAR>ha : a % 4 = 1<VAR>hb : Odd b<GOAL>jacobiSym (↑a) b = jacobiSym (↑b) a
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : b % 4 = 1<GOAL>jacobiSym (↑a) b = jacobiSym (↑b) a
<VAR>a b : ℕ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<GOAL>jacobiSym (↑a) b = -jacobiSym (↑b) a
<VAR>a b : ℕ<VAR>ha2 : a % 2 = 1<VAR>hb2 : b % 2 = 1<GOAL>(if a % 4 = 3 ∧ b % 4 = 3 then -jacobiSym (↑b) a else jacobiSym (↑b) a) = jacobiSym (↑a) b
<VAR>a : ℕ<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym (↑a) b = jacobiSym (↑a) (b % (4 * a))
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym a b = jacobiSym a (b % (4 * a.natAbs))
<VAR>a b : ℕ<VAR>flip : Bool<VAR>ha0 : a > 0<VAR>hb2 : b % 2 = 1<VAR>hb1 : b > 1<GOAL>fastJacobiSymAux a b flip ha0 = if flip = true then -jacobiSym (↑a) b else jacobiSym (↑a) b
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<GOAL>(NumberField.basisMatrix K).det ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>α : K<GOAL>(NumberField.canonicalEmbedding K) α = (NumberField.basisMatrix K).transpose.mulVec fun i => ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr α) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>DecidableEq (K →+* ℂ)<VAR>α : NumberField.RingOfIntegers K<VAR>i : K →+* ℂ<GOAL>(NumberField.basisMatrix K).transpose⁻¹.mulVec (fun j => (NumberField.canonicalEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) α) j) i = ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr ↑α) i)
<VAR>K : Type u_1<VAR>Field K<VAR>self : NumberField K<GOAL>CharZero K
<VAR>K : Type u_1<VAR>Field K<VAR>self : NumberField K<GOAL>FiniteDimensional ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<GOAL>Algebra.IsAlgebraic ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>x : NumberField.RingOfIntegers K<GOAL>↑x = (algebraMap (NumberField.RingOfIntegers K) K) x
<VAR>K : Type u_1<VAR>Field K<VAR>x y : NumberField.RingOfIntegers K<VAR>h : ↑x = ↑y<GOAL>x = y
<VAR>K : Type u_1<VAR>Field K<VAR>x y : NumberField.RingOfIntegers K<GOAL>x = y ↔ ↑x = ↑y
<VAR>K : Type u_1<VAR>Field K<VAR>x y : NumberField.RingOfIntegers K<GOAL>↑x = ↑y ↔ x = y
<VAR>K : Type u_1<VAR>Field K<VAR>x : K<VAR>hx : x ∈ integralClosure ℤ K<GOAL>(algebraMap (NumberField.RingOfIntegers K) K) ⟨x, hx⟩ = x
<VAR>K : Type u_1<VAR>Field K<VAR>x : K<VAR>hx : x ∈ integralClosure ℤ K<GOAL>↑⟨x, hx⟩ = x
<VAR>K : Type u_1<VAR>Field K<VAR>x y : K<VAR>hx : x ∈ integralClosure ℤ K<VAR>hy : y ∈ integralClosure ℤ K<GOAL>⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y
<VAR>K : Type u_1<VAR>Field K<GOAL>⟨1, ⋯⟩ = 1
<VAR>K : Type u_1<VAR>Field K<GOAL>⟨0, ⋯⟩ = 0
<VAR>K : Type u_1<VAR>Field K<VAR>x y : K<VAR>hx : x ∈ integralClosure ℤ K<VAR>hy : y ∈ integralClosure ℤ K<GOAL>⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
<VAR>K : Type u_1<VAR>Field K<VAR>x y : K<VAR>hx : x ∈ integralClosure ℤ K<VAR>hy : y ∈ integralClosure ℤ K<GOAL>⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
<VAR>K : Type u_1<VAR>Field K<VAR>x y : K<VAR>hx : x ∈ integralClosure ℤ K<VAR>hy : y ∈ integralClosure ℤ K<GOAL>⟨x, hx⟩ - ⟨y, hy⟩ = ⟨x - y, ⋯⟩
<VAR>K : Type u_1<VAR>Field K<VAR>x : K<VAR>hx : x ∈ integralClosure ℤ K<GOAL>-⟨x, hx⟩ = ⟨-x, ⋯⟩
<VAR>K : Type u_1<VAR>Field K<GOAL>Function.Injective ⇑(algebraMap (NumberField.RingOfIntegers K) K)
<VAR>K : Type u_1<VAR>Field K<VAR>x : NumberField.RingOfIntegers K<GOAL>(algebraMap (NumberField.RingOfIntegers K) K) x = 0 ↔ x = 0
<VAR>K : Type u_1<VAR>Field K<VAR>x : NumberField.RingOfIntegers K<GOAL>(algebraMap (NumberField.RingOfIntegers K) K) x ≠ 0 ↔ x ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>x : NumberField.RingOfIntegers K<GOAL>IsIntegral ℤ ((algebraMap (NumberField.RingOfIntegers K) K) x)
<VAR>K : Type u_1<VAR>Field K<VAR>x : NumberField.RingOfIntegers K<GOAL>IsIntegral ℤ x
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<GOAL>¬IsField (NumberField.RingOfIntegers K)
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>(NumberField.integralBasis K) i = (algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.RingOfIntegers.basis K) i)
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<VAR>x : NumberField.RingOfIntegers K<VAR>i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)<GOAL>((NumberField.integralBasis K).repr ((algebraMap (NumberField.RingOfIntegers K) K) x)) i = (algebraMap ℤ ℚ) (((NumberField.RingOfIntegers.basis K).repr x) i)
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<VAR>x : K<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.integralBasis K)) ↔ x ∈ (algebraMap (NumberField.RingOfIntegers K) K).range
<VAR>K : Type u_1<VAR>Field K<VAR>nf : NumberField K<GOAL>FiniteDimensional.finrank ℤ (NumberField.RingOfIntegers K) = FiniteDimensional.finrank ℚ K
<VAR>f g : MulRingNorm ℚ<GOAL>(∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n
<VAR>f g : MulRingNorm ℚ<GOAL>(∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.equiv g
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>(Rat.MulRingNorm.mulRingNorm_padic p) r = ↑(padicNorm p r)
<VAR>f : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<GOAL>∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
<VAR>f : MulRingNorm ℚ<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>Nat.Prime p
<VAR>f : MulRingNorm ℚ<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>m : ℕ<VAR>hpm : ¬p ∣ m<GOAL>f ↑m = 1
<VAR>f : MulRingNorm ℚ<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)
<VAR>f : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (Rat.MulRingNorm.mulRingNorm_padic p)
<VAR>n b : ℕ<VAR>h : n.ProbablePrime b<VAR>h₁ : 1 ≤ n<VAR>h₂ : 1 ≤ b<GOAL>n.Coprime b
<VAR>n : ℕ<VAR>b : ℕ<VAR>h : 1 ≤ b<GOAL>n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
<VAR>n b : ℕ<VAR>h : n.FermatPsp b<VAR>h₁ : 1 ≤ b<GOAL>n.Coprime b
<VAR>n : ℕ<VAR>h₁ : 1 < n<VAR>h₂ : ¬Nat.Prime n<GOAL>n.FermatPsp 1
<VAR>a b : ℕ<VAR>ha : 2 ≤ a<VAR>hb : 2 ≤ b<GOAL>2 ≤ (a ^ b - 1) / (a - 1)
<VAR>b p : ℕ<GOAL>2 ≤ b → Odd p → (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<GOAL>b ^ (2 * p) - 1 - (b ^ 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<GOAL>(Nat.psp_from_prime b p).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>p_gt_two : 2 < p<GOAL>p < Nat.psp_from_prime b p
<VAR>b : ℕ<VAR>h : 1 ≤ b<VAR>m : ℕ<GOAL>∃ n, n.FermatPsp b ∧ m ≤ n
<VAR>b : ℕ<VAR>h : 1 ≤ b<GOAL>{n | n.FermatPsp b}.Infinite
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.classNumber K = 1 ↔ IsPrincipalIdealRing (NumberField.RingOfIntegers K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>C : ClassGroup (NumberField.RingOfIntegers K)<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * (↑(FiniteDimensional.finrank ℚ K).factorial / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * √|↑(NumberField.discr K)|)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>h : ↑|NumberField.discr K| < (2 * (Real.pi / 4) ^ NumberField.InfinitePlace.NrComplexPlaces K * (↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K / ↑(FiniteDimensional.finrank ℚ K).factorial)) ^ 2<GOAL>IsPrincipalIdealRing (NumberField.RingOfIntegers K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I<GOAL>(NumberField.basisOfFractionalIdeal K I) i = ↑((NumberField.fractionalIdealBasis K ↑I) i)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>x : K<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<GOAL>FiniteDimensional.finrank ℤ ↥↑↑I = FiniteDimensional.finrank ℤ (NumberField.RingOfIntegers K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I<GOAL>|(NumberField.integralBasis K).det ⇑((NumberField.basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm ↑I
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.Units.regulator K ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>0 < NumberField.Units.regulator K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>e : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } ≃ Fin (NumberField.Units.rank K)<GOAL>NumberField.Units.regulator K = |(Matrix.of fun i => (NumberField.Units.logEmbedding K) (NumberField.Units.fundSystem K (e i))).det|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>u : Fin (NumberField.Units.rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : NumberField.InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (NumberField.Units.rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (NumberField.Units.rank K)<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w' : NumberField.InfinitePlace K<VAR>e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)<GOAL>NumberField.Units.regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(NumberField.Units.fundSystem K (e i))))).det|
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
<VAR>ξ : ℚ<GOAL>{q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite
<VAR>ξ : ℝ<GOAL>ξ.convergent 0 = ↑⌊ξ⌋
<VAR>ξ : ℝ<VAR>n : ℕ<GOAL>ξ.convergent (n + 1) = ↑⌊ξ⌋ + ((Int.fract ξ)⁻¹.convergent n)⁻¹
<VAR>n : ℕ<GOAL>Real.convergent 0 n = 0
<VAR>ξ : ℤ<VAR>n : ℕ<GOAL>(↑ξ).convergent n = ↑ξ
<VAR>ξ : ℝ<VAR>n : ℕ<GOAL>(GenContFract.of ξ).convs n = ↑(ξ.convergent n)
<VAR>v : ℤ<VAR>hv : 0 < v<GOAL>0 < ↑v ∧ 0 < 2 * ↑v - 1
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : Real.ContfracLegendre.Ass ξ u v<GOAL>0 < Int.fract ξ
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : Real.ContfracLegendre.Ass ξ u v<GOAL>0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : Real.ContfracLegendre.Ass ξ u v<GOAL>|(Int.fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : Real.ContfracLegendre.Ass ξ u v<GOAL>Real.ContfracLegendre.Ass (Int.fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
<VAR>ξ : ℝ<VAR>u : ℤ<VAR>v : ℕ<VAR>h' : Real.ContfracLegendre.Ass ξ u ↑v<GOAL>∃ n, ↑u / ↑v = ξ.convergent n
<VAR>ξ : ℝ<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>∃ n, q = ξ.convergent n
<VAR>ξ : ℝ<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>∃ n, (GenContFract.of ξ).convs n = ↑q
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = L (fun n => χ ↑n) s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>∏' (p : Nat.Primes), (1 - ↑↑p ^ (-s))⁻¹ = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) Filter.atTop (𝓝 (riemannZeta s))
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = L (fun n => χ ↑n) s
<VAR>s : ℂ<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>hs : 1 < s.re<GOAL>Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (𝓝 (L (fun n => χ ↑n) s))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>↑(p - 1)! = -1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>∏ x ∈ Finset.Ico 1 p, ↑x = -1
<VAR>n : ℕ<VAR>h : ↑(n - 1)! = -1<VAR>h1 : n ≠ 1<GOAL>Nat.Prime n
<VAR>n : ℕ<VAR>h : n ≠ 1<GOAL>Nat.Prime n ↔ ↑(n - 1)! = -1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : 𝓞 K<GOAL>↑((Algebra.norm ℤ) x) = (Algebra.norm ℚ) ↑x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : 𝓞 K<GOAL>↑((Algebra.trace ℤ (𝓞 K)) x) = (Algebra.trace ℚ K) ↑x
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : 𝓞 L<GOAL>↑((RingOfIntegers.norm K) x) = (Algebra.norm K) ↑x
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : 𝓞 L<GOAL>↑((algebraMap (𝓞 K) (𝓞 L)) ((RingOfIntegers.norm K) x)) = (algebraMap K L) ((Algebra.norm K) ↑x)
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : 𝓞 K<GOAL>(algebraMap (𝓞 K) K) ((RingOfIntegers.norm K) ((algebraMap (𝓞 K) (𝓞 L)) x)) = (Algebra.norm K) ((algebraMap K L) ((algebraMap (𝓞 K) K) x))
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : 𝓞 K<GOAL>(RingOfIntegers.norm K) ((algebraMap (𝓞 K) (𝓞 L)) x) = x ^ FiniteDimensional.finrank K L
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>IsGalois K L<VAR>x : 𝓞 L<GOAL>IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>IsGalois K L<VAR>x : 𝓞 L<GOAL>x ∣ (algebraMap (𝓞 K) (𝓞 L)) ((RingOfIntegers.norm K) x)
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>F : Type u_3<VAR>Field F<VAR>Algebra K F<VAR>Algebra.IsSeparable K F<VAR>FiniteDimensional K F<VAR>Algebra.IsSeparable K L<VAR>Algebra F L<VAR>Algebra.IsSeparable F L<VAR>FiniteDimensional F L<VAR>IsScalarTower K F L<VAR>x : 𝓞 L<GOAL>(RingOfIntegers.norm K) ((RingOfIntegers.norm F) x) = (RingOfIntegers.norm K) x
<VAR>K : Type u_2<VAR>Field K<VAR>F : Type u_3<VAR>Field F<VAR>Algebra K F<VAR>Algebra.IsSeparable K F<VAR>FiniteDimensional K F<VAR>CharZero K<VAR>x : 𝓞 F<GOAL>IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x
<VAR>a b c : ℤ<GOAL>Fermat42 a b c ↔ Fermat42 b a c
<VAR>a b c k : ℤ<VAR>hk0 : k ≠ 0<GOAL>Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c)
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0
<VAR>a b c : ℤ<VAR>h : Fermat42.Minimal a b c<GOAL>IsCoprime a b
<VAR>a b c : ℤ<GOAL>Fermat42.Minimal a b c → Fermat42.Minimal b a c
<VAR>a b c : ℤ<GOAL>Fermat42.Minimal a b c → Fermat42.Minimal a b (-c)
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>r s : ℤ<VAR>h2 : IsCoprime s r<GOAL>IsCoprime (r ^ 2 + s ^ 2) r
<VAR>a b c : ℤ<VAR>h : Fermat42.Minimal a b c<VAR>ha2 : a % 2 = 1<VAR>hc : 0 < c<GOAL>False
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a ^ 4 + b ^ 4 ≠ c ^ 2
<VAR>hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p<GOAL>FermatLastTheorem
<VAR>R : Type u<VAR>CommRing R<VAR>W : ℤ → R<VAR>h : IsEllSequence W<VAR>x : R<GOAL>IsEllSequence (x • W)
<VAR>R : Type u<VAR>CommRing R<VAR>W : ℤ → R<VAR>h : IsDivSequence W<VAR>x : R<GOAL>IsDivSequence (x • W)
<VAR>R : Type u<VAR>CommRing R<VAR>W : ℤ → R<VAR>h : IsEllDivSequence W<VAR>x : R<GOAL>IsEllDivSequence (x • W)
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS' b c d 0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS' b c d 1 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS' b c d 2 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS' b c d 3 = c
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS' b c d 4 = d
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS' b c d (2 * (m + 2) + 1) = (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS' b c d (2 * (m + 3)) = preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>n : ℕ<GOAL>preNormEDS b c d ↑n = preNormEDS' b c d n
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS b c d 0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS b c d 1 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS b c d 2 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS b c d 3 = c
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>preNormEDS b c d 4 = d
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS b c d (2 * (↑m + 2) + 1) = (preNormEDS b c d (↑m + 4) * preNormEDS b c d (↑m + 2) ^ 3 * if Even m then b else 1) - preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) ^ 3 * if Even m then 1 else b
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS b c d (2 * (↑m + 3)) = preNormEDS b c d (↑m + 2) ^ 2 * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 5) - preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) * preNormEDS b c d (↑m + 4) ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>n : ℤ<GOAL>preNormEDS b c d (-n) = -preNormEDS b c d n
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>n : ℕ<GOAL>normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>normEDS b c d 0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>normEDS b c d 1 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>normEDS b c d 2 = b
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>normEDS b c d 3 = c
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<GOAL>normEDS b c d 4 = d * b
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>normEDS b c d (2 * (↑m + 2) + 1) = normEDS b c d (↑m + 4) * normEDS b c d (↑m + 2) ^ 3 - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>m : ℕ<GOAL>normEDS b c d (2 * (↑m + 3)) * b = normEDS b c d (↑m + 2) ^ 2 * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 5) - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 4) ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>b c d : R<VAR>n : ℤ<GOAL>normEDS b c d (-n) = -normEDS b c d n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℕ<GOAL>f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>f (normEDS b c d n) = normEDS (f b) (f c) (f d) n
<VAR>f : ℕ → ℂ<VAR>n : ℕ<VAR>s : ℂ<GOAL>HasDerivAt (fun z => LSeries.term f z n) (-LSeries.term (LSeries.logMul f) s n) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>LSeriesSummable (LSeries.logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>deriv (LSeries f) s = -LSeries (LSeries.logMul f) s
<VAR>f : ℕ → ℂ<GOAL>Set.EqOn (deriv (LSeries f)) (-LSeries (LSeries.logMul f)) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>LSeriesSummable (LSeries.logMul f) s
<VAR>f : ℕ → ℂ<GOAL>LSeries.abscissaOfAbsConv (LSeries.logMul f) = LSeries.abscissaOfAbsConv f
<VAR>f : ℕ → ℂ<VAR>m : ℕ<GOAL>LSeries.abscissaOfAbsConv (LSeries.logMul^[m] f) = LSeries.abscissaOfAbsConv f
<VAR>f : ℕ → ℂ<VAR>m : ℕ<VAR>s : ℂ<VAR>h : LSeries.abscissaOfAbsConv f < ↑s.re<GOAL>iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (LSeries.logMul^[m] f) s
<VAR>f : ℕ → ℂ<GOAL>DifferentiableOn ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
<VAR>f : ℕ → ℂ<GOAL>AnalyticOn ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re}
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p % 4 ≠ 3<GOAL>∃ a b, a ^ 2 + b ^ 2 = p
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b x y u v : R<VAR>ha : a = x ^ 2 + y ^ 2<VAR>hb : b = u ^ 2 + v ^ 2<GOAL>∃ r s, a * b = r ^ 2 + s ^ 2
<VAR>a b x y u v : ℕ<VAR>ha : a = x ^ 2 + y ^ 2<VAR>hb : b = u ^ 2 + v ^ 2<GOAL>∃ r s, a * b = r ^ 2 + s ^ 2
<VAR>m n : ℕ<VAR>hd : m ∣ n<VAR>hs : IsSquare (-1)<GOAL>IsSquare (-1)
<VAR>m n : ℕ<VAR>hc : m.Coprime n<VAR>hm : IsSquare (-1)<VAR>hn : IsSquare (-1)<GOAL>IsSquare (-1)
<VAR>p n : ℕ<VAR>hpp : Nat.Prime p<VAR>hp : p ∣ n<VAR>hs : IsSquare (-1)<GOAL>p % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
<VAR>n x y : ℕ<VAR>h : n = x ^ 2 + y ^ 2<VAR>hc : x.Coprime y<GOAL>IsSquare (-1)
<VAR>n : ℕ<GOAL>(∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
<VAR>n : ℕ<GOAL>(∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Nat.Prime q → q % 4 = 3 → Even (padicValNat q n)
<VAR>R : Type u_1<VAR>Zero R<VAR>f f' : ℕ → R<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n<GOAL>toArithmeticFunction f = toArithmeticFunction f'
<VAR>R : Type u_1<VAR>Zero R<VAR>f : ArithmeticFunction R<GOAL>toArithmeticFunction ⇑f = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>f f' g g' : ℕ → R<VAR>hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n<VAR>hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n<GOAL>f ⍟ g = f' ⍟ g'
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ArithmeticFunction R<GOAL>⇑f ⍟ ⇑g = ⇑(f * g)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ℕ → R<GOAL>f ⍟ g = fun n => ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ℕ → R<GOAL>(f ⍟ g) 0 = 0
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>LSeries.term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, LSeries.term f s p.1 * LSeries.term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries.term (f ⍟ g) s = fun n => ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), LSeries.term f s (↑b).1 * LSeries.term g s (↑b).2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>L (f ⍟ g) s = L f s * L g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeries.abscissaOfAbsConv f < ↑s.re<VAR>hg : LSeries.abscissaOfAbsConv g < ↑s.re<GOAL>L (f ⍟ g) s = L f s * L g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>LSeriesSummable (f ⍟ g) s
<VAR>f g : ArithmeticFunction ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum (fun n => f n) s a<VAR>hg : LSeriesHasSum (fun n => g n) s b<GOAL>LSeriesHasSum (fun n => (f * g) n) s (a * b)
<VAR>f g : ArithmeticFunction ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable (fun n => f n) s<VAR>hg : LSeriesSummable (fun n => g n) s<GOAL>L (fun n => (f * g) n) s = L (fun n => f n) s * L (fun n => g n) s
<VAR>f g : ArithmeticFunction ℂ<VAR>s : ℂ<VAR>hf : (LSeries.abscissaOfAbsConv fun n => f n) < ↑s.re<VAR>hg : (LSeries.abscissaOfAbsConv fun n => g n) < ↑s.re<GOAL>L (fun n => (f * g) n) s = L (fun n => f n) s * L (fun n => g n) s
<VAR>f g : ArithmeticFunction ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable (fun n => f n) s<VAR>hg : LSeriesSummable (fun n => g n) s<GOAL>LSeriesSummable (fun n => (f * g) n) s
<VAR>n : ℤ<VAR>z τ : ℂ<GOAL>HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)
<VAR>S : ℝ<VAR>T : ℝ<VAR>hT : 0 < T<VAR>k : ℕ<GOAL>Summable fun n => ↑|n| ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
<VAR>z τ : ℂ<GOAL>(Summable fun x => jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im
<VAR>z τ : ℂ<GOAL>(Summable fun x => jacobiTheta₂'_term x z τ) ↔ 0 < τ.im
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasSum (fun n => jacobiTheta₂_term n z τ) (jacobiTheta₂ z τ)
<VAR>z : ℂ<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasSum (fun n => jacobiTheta₂_term_fderiv n z τ) (jacobiTheta₂_fderiv z τ)