ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>f : ℕ → F<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>s : Finset ℕ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hs : p ∉ s<VAR>e : ℕ<VAR>m : ↑(Nat.factoredNumbers s)<GOAL>f (p ^ e * ↑m) = f (p ^ e) * f ↑m
<VAR>s : Finset ℕ<VAR>p e m : ℕ<VAR>hp : Nat.Prime p<VAR>hs : p ∉ s<VAR>hm : m ∈ Nat.factoredNumbers s<GOAL>↑((Nat.equivProdNatFactoredNumbers hp hs) (e, ⟨m, hm⟩)) = p ^ e * m
<VAR>s : Finset ℕ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hs : p ∉ s<VAR>x : ℕ × ↑(Nat.factoredNumbers s)<GOAL>↑((Nat.equivProdNatFactoredNumbers hp hs) x) = p ^ x.1 * ↑x.2
<VAR>n m : ℕ<GOAL>m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n
<VAR>n : ℕ<GOAL>n.smoothNumbers = Nat.factoredNumbers (Finset.range n)
<VAR>n : ℕ<GOAL>n.smoothNumbers = Nat.factoredNumbers n.primesBelow
<VAR>n m : ℕ<GOAL>m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p < n
<VAR>n m : ℕ<GOAL>m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ m → p < n
<VAR>m n : ℕ<VAR>hms : m ∈ n.smoothNumbers<GOAL>m.primeFactors ⊆ n.primesBelow
<VAR>m n : ℕ<VAR>hm : m ≠ 0<VAR>hp : m.primeFactors ⊆ Finset.range n<GOAL>m ∈ n.smoothNumbers
<VAR>m n : ℕ<GOAL>m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ m.primeFactors ⊆ n.primesBelow
<VAR>n m : ℕ<VAR>h : m ∈ n.smoothNumbers<GOAL>m ≠ 0
<VAR>N : ℕ<VAR>hN : ¬Nat.Prime N<GOAL>N.succ.smoothNumbers = N.smoothNumbers
<VAR>N M : ℕ<VAR>hNM : N ≤ M<GOAL>N.smoothNumbers ⊆ M.smoothNumbers
<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>hmn : m < n<GOAL>m ∈ n.smoothNumbers
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<GOAL>p ^ e * n ∈ p.succ.smoothNumbers
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hn : n ∈ p.smoothNumbers<GOAL>p.Coprime n
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>f : ℕ → F<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>e : ℕ<VAR>m : ↑p.smoothNumbers<GOAL>f (p ^ e * ↑m) = f (p ^ e) * f ↑m
<VAR>p e m : ℕ<VAR>hp : Nat.Prime p<VAR>hm : m ∈ p.smoothNumbers<GOAL>↑((Nat.equivProdNatSmoothNumbers hp) (e, ⟨m, hm⟩)) = p ^ e * m
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>x : ℕ × ↑p.smoothNumbers<GOAL>↑((Nat.equivProdNatSmoothNumbers hp) x) = p ^ x.1 * ↑x.2
<VAR>N k : ℕ<GOAL>N.smoothNumbersUpTo k ⊆ Finset.image (fun x => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)
<VAR>N k : ℕ<GOAL>N.roughNumbersUpTo k = (N.succ.primesBelow \ k.primesBelow).biUnion fun p => Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)
<VAR>N k : ℕ<GOAL>(N.roughNumbersUpTo k).card ≤ ∑ p ∈ N.succ.primesBelow \ k.primesBelow, N / p
<VAR>p q r : ℕ+<GOAL>ADEInequality.sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹
<VAR>q r : ℕ+<GOAL>ADEInequality.Admissible (ADEInequality.A' q r)
<VAR>n : ℕ+<GOAL>ADEInequality.Admissible (ADEInequality.D' n)
<GOAL>ADEInequality.Admissible (ADEInequality.E' 3)
<GOAL>ADEInequality.Admissible (ADEInequality.E' 4)
<GOAL>ADEInequality.Admissible (ADEInequality.E' 5)
<GOAL>ADEInequality.Admissible ADEInequality.E6
<GOAL>ADEInequality.Admissible ADEInequality.E7
<GOAL>ADEInequality.Admissible ADEInequality.E8
<VAR>pqr : Multiset ℕ+<GOAL>ADEInequality.Admissible pqr → 1 < ADEInequality.sumInv pqr
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>H : 1 < ADEInequality.sumInv {p, q, r}<GOAL>p < 3
<VAR>q r : ℕ+<VAR>hqr : q ≤ r<VAR>H : 1 < ADEInequality.sumInv {2, q, r}<GOAL>q < 4
<VAR>r : ℕ+<VAR>H : 1 < ADEInequality.sumInv {2, 3, r}<GOAL>r < 6
<VAR>p q r : ℕ+<VAR>hpq : p ≤ q<VAR>hqr : q ≤ r<VAR>H : 1 < ADEInequality.sumInv {p, q, r}<GOAL>ADEInequality.Admissible {p, q, r}
<VAR>pqr : List ℕ+<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) pqr → pqr.length = 3 → 1 < ADEInequality.sumInv ↑pqr → ADEInequality.Admissible ↑pqr
<VAR>p q r : ℕ+<VAR>H : 1 < ADEInequality.sumInv {p, q, r}<GOAL>ADEInequality.Admissible {p, q, r}
<VAR>p q r : ℕ+<GOAL>1 < ADEInequality.sumInv {p, q, r} ↔ ADEInequality.Admissible {p, q, r}
<VAR>α : Type u_1<VAR>Semiring α<VAR>NoZeroDivisors α<VAR>m n : ℕ<VAR>hmn : m ∣ n<VAR>hm : FermatLastTheoremWith α m<GOAL>FermatLastTheoremWith α n
<VAR>m n : ℕ<VAR>hmn : m ∣ n<VAR>hm : FermatLastTheoremFor m<GOAL>FermatLastTheoremFor n
<VAR>n : ℕ<GOAL>[FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
<VAR>n : ℕ<GOAL>FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n
<VAR>n : ℕ<GOAL>FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n
<VAR>n : ℕ<GOAL>FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n
<VAR>n : ℕ<VAR>R : Type u_2<VAR>CommSemiring R<VAR>IsDomain R<VAR>DecidableEq R<VAR>NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<GOAL>FermatLastTheoremWith R n
<VAR>n : ℕ<VAR>p : ℤ<VAR>hp : Prime p<VAR>a b c : ℤ<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<VAR>HF : a ^ n + b ^ n + c ^ n = 0<GOAL>p ∣ c
<VAR>n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ n + b ^ n + c ^ n = 0<GOAL>IsCoprime a b
<VAR>n : ℕ<VAR>f : ℕ → ℕ<VAR>hf' : ∀ k < n, Squarefree (f k)<GOAL>n.GrahamConjecture f
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Finset.filter (fun x => x ∣ n) (Finset.range n.succ) = n.divisors
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Finset.filter (fun x => x ∣ n) (Finset.range n) = n.properDivisors
<VAR>n : ℕ<GOAL>n ∉ n.properDivisors
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Finset.cons n n.properDivisors ⋯ = n.divisors
<VAR>n : ℕ<GOAL>1 ∈ n.divisors ↔ n ≠ 0
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>n ∈ n.divisors
<VAR>n m : ℕ<VAR>h : n ∈ m.divisors<GOAL>n ∣ m
<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>p.1 ≠ 0
<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>p.2 ≠ 0
<VAR>n m : ℕ<GOAL>n ∈ m.divisors → n ≤ m
<VAR>n m : ℕ<VAR>hzero : n ≠ 0<VAR>h : m ∣ n<GOAL>m.divisors ⊆ n.divisors
<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ∣ n<GOAL>Finset.filter (fun x => x ∣ m) n.divisors = m.divisors
<VAR>n : ℕ<GOAL>n.divisors.Nonempty ↔ n ≠ 0
<VAR>n : ℕ<GOAL>n.divisors = ∅ ↔ n = 0
<VAR>n : ℕ<GOAL>n.properDivisors ⊆ n.divisors
<VAR>n m : ℕ<VAR>h : m ∈ n.divisors<GOAL>0 < m
<VAR>n m : ℕ<VAR>h : m ∈ n.properDivisors<GOAL>0 < m
<VAR>n : ℕ<GOAL>n.divisors.sup id = n
<VAR>m n : ℕ<VAR>h : m ∈ n.properDivisors<GOAL>1 < n
<VAR>m n : ℕ<VAR>h : m ∈ n.properDivisors<GOAL>1 < n / m
<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k
<VAR>n : ℕ<GOAL>n.properDivisors.Nonempty ↔ 1 < n
<GOAL>Nat.divisorsAntidiagonal 1 = {(1, 1)}
<VAR>n : ℕ<GOAL>Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
<VAR>n : ℕ<GOAL>Finset.image Prod.fst n.divisorsAntidiagonal = n.divisors
<VAR>n : ℕ<GOAL>Finset.image Prod.snd n.divisorsAntidiagonal = n.divisors
<VAR>n : ℕ<GOAL>Finset.map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
<VAR>n : ℕ<GOAL>Finset.map { toFun := fun d => (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>n.Perfect ↔ ∑ i ∈ n.properDivisors, i = n
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>k : ℕ<VAR>x : ℕ<GOAL>x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>p.divisors = {1, p}
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>p.properDivisors = {1}
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>k : ℕ<GOAL>(p ^ k).divisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range (k + 1))
<VAR>a b : ℕ<GOAL>a.divisors = b.divisors ↔ a = b
<VAR>n : ℕ<VAR>s : Finset ℕ<VAR>hsub : s ⊆ n.properDivisors<GOAL>∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors
<VAR>n : ℕ<VAR>h : ∑ x ∈ n.properDivisors, x ∣ n<GOAL>∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∑ x ∈ p.properDivisors, f x = f 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∏ x ∈ p.properDivisors, f x = f 1
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∑ x ∈ p.divisors, f x = f p + f 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∏ x ∈ p.divisors, f x = f p * f 1
<VAR>n : ℕ<GOAL>n.properDivisors = {1} ↔ Nat.Prime n
<VAR>n : ℕ<GOAL>∑ x ∈ n.properDivisors, x = 1 ↔ Nat.Prime n
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>k : ℕ<VAR>x : ℕ<GOAL>x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>k : ℕ<GOAL>(p ^ k).properDivisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range k)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ Finset.range k, f (p ^ x)
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∑ x ∈ (p ^ k).properDivisors, f x = ∑ x ∈ Finset.range k, f (p ^ x)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ Finset.range (k + 1), f (p ^ x)
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Nat.Prime p<GOAL>∑ x ∈ (p ^ k).divisors, f x = ∑ x ∈ Finset.range (k + 1), f (p ^ x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f i (n / i)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f (n / i) i
<VAR>n : ℕ<GOAL>n.primeFactors = Finset.filter Nat.Prime n.divisors
<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>hmn : m ∣ n<GOAL>Finset.filter (fun x => x ∣ m) n.primeFactors = m.primeFactors
<VAR>n : ℕ<GOAL>Finset.image (fun x => n / x) n.divisors = n.divisors
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>n : ℕ<VAR>f : ℕ → α<GOAL>∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>f : ℕ → α<GOAL>∑ d ∈ n.divisors, f (n / d) = n.divisors.sum f
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<GOAL>x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>q : ℕ<VAR>p : ℕ<VAR>prime_p : Nat.Prime p<VAR>covering : p ≤ 2 * q<VAR>H : n < q → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>hn : n < p<GOAL>∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>hn0 : n ≠ 0<GOAL>∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : 𝓞 K<GOAL>IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1
<VAR>K : Type u_1<VAR>Field K<GOAL>Function.Injective fun x => (algebraMap (𝓞 K) K) ↑x
<VAR>K : Type u_1<VAR>Field K<VAR>u : (𝓞 K)ˣ<GOAL>↑↑u = (algebraMap (𝓞 K) K) ↑u
<VAR>K : Type u_1<VAR>Field K<VAR>x y : (𝓞 K)ˣ<GOAL>(algebraMap (𝓞 K) K) ↑(x * y) = (algebraMap (𝓞 K) K) ↑x * (algebraMap (𝓞 K) K) ↑y
<VAR>K : Type u_1<VAR>Field K<VAR>x : (𝓞 K)ˣ<VAR>n : ℕ<GOAL>(algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
<VAR>K : Type u_1<VAR>Field K<VAR>x : (𝓞 K)ˣ<VAR>n : ℤ<GOAL>(algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
<VAR>K : Type u_1<VAR>Field K<GOAL>(algebraMap (𝓞 K) K) ↑1 = 1
<VAR>K : Type u_1<VAR>Field K<GOAL>(algebraMap (𝓞 K) K) ↑(-1) = -1
<VAR>K : Type u_1<VAR>Field K<VAR>x : (𝓞 K)ˣ<GOAL>(algebraMap (𝓞 K) K) ↑x ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑x)| = 1
<VAR>K : Type u_1<VAR>Field K<VAR>x : (𝓞 K)ˣ<VAR>NumberField K<GOAL>x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>k : ℕ+<VAR>hc : (↑k).Coprime ↑(NumberField.Units.torsionOrder K)<VAR>ζ : (𝓞 K)ˣ<GOAL>ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>rootsOfUnity (NumberField.Units.torsionOrder K) (𝓞 K) = NumberField.Units.torsion K
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>a.x ^ 2 - d * a.y ^ 2 = 1
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>a.x ^ 2 = 1 + d * a.y ^ 2
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>d * a.y ^ 2 = a.x ^ 2 - 1
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<VAR>hx : a.x = b.x<VAR>hy : a.y = b.y<GOAL>a = b
<VAR>d : ℤ<VAR>x y : ℤ<VAR>prop : x ^ 2 - d * y ^ 2 = 1<GOAL>(Pell.Solution₁.mk x y prop).x = x
<VAR>d : ℤ<VAR>x y : ℤ<VAR>prop : x ^ 2 - d * y ^ 2 = 1<GOAL>(Pell.Solution₁.mk x y prop).y = y
<VAR>d : ℤ<VAR>x y : ℤ<VAR>prop : x ^ 2 - d * y ^ 2 = 1<GOAL>↑(Pell.Solution₁.mk x y prop) = { re := x, im := y }
<VAR>d : ℤ<GOAL>Pell.Solution₁.x 1 = 1
<VAR>d : ℤ<GOAL>Pell.Solution₁.y 1 = 0
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<GOAL>(a * b).x = a.x * b.x + d * (a.y * b.y)
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<GOAL>(a * b).y = a.x * b.y + a.y * b.x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>a⁻¹.x = a.x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>a⁻¹.y = -a.y
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>(-a).x = -a.x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>(-a).y = -a.y
<VAR>d : ℤ<VAR>h₀ : d < 0<VAR>a : Pell.Solution₁ d<GOAL>a.x = 0 ∨ a.y = 0
<VAR>d : ℤ<VAR>h₀ : 0 ≤ d<VAR>a : Pell.Solution₁ d<GOAL>a.x ≠ 0
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>ha : 1 < a.x<GOAL>a.y ≠ 0
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>ha : 1 < a.x<GOAL>0 < d
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>ha : 1 < a.x<GOAL>¬IsSquare d
<VAR>d : ℤ<VAR>h₀ : d ≠ 0<VAR>a : Pell.Solution₁ d<VAR>ha : a.x = 1<GOAL>a = 1
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>a = 1 ∨ a = -1 ↔ a.y = 0
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<VAR>ha : 0 < a.x<VAR>hb : 0 < b.x<GOAL>0 < (a * b).x
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>hbx : 0 < b.x<VAR>hby : 0 < b.y<GOAL>0 < (a * b).y
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>n : ℕ<GOAL>0 < (a ^ n).x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>n : ℕ<GOAL>0 < (a ^ n.succ).y
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>n : ℤ<VAR>hn : 0 < n<GOAL>0 < (a ^ n).y
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>n : ℤ<GOAL>0 < (a ^ n).x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>n : ℤ<GOAL>(a ^ n).y.sign = n.sign
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>a : Pell.Solution₁ d<GOAL>∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<GOAL>0 < a.x
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<GOAL>0 < d
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<GOAL>¬IsSquare d
<VAR>d : ℤ<VAR>a b : Pell.Solution₁ d<VAR>ha : Pell.IsFundamental a<VAR>hb : Pell.IsFundamental b<GOAL>a = b
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃ a, Pell.IsFundamental a
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<GOAL>StrictMono fun n => (a ^ n).y
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<VAR>m n : ℤ<GOAL>(a ^ m).y < (a ^ n).y ↔ m < n
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<VAR>n : ℤ<GOAL>a ^ n = 1 ↔ n = 0
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a<VAR>n n' : ℤ<GOAL>a ^ n ≠ -a ^ n'
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<GOAL>a₁.x ≤ a.x
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a₁.y ≤ a.y
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.x * a₁.y ≤ a.y * a₁.x
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 ≤ (a * a₁⁻¹).y
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 < (a * a₁⁻¹).x
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>(a * a₁⁻¹).x < a.x
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 ≤ a.y<GOAL>∃ n, a = a₁ ^ n
<VAR>d : ℤ<VAR>a₁ : Pell.Solution₁ d<VAR>h : Pell.IsFundamental a₁<VAR>a : Pell.Solution₁ d<GOAL>∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Pell.Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>a : Pell.Solution₁ d<GOAL>(1 < a.x ∧ 0 < a.y ∧ ∀ (b : Pell.Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ Pell.IsFundamental a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>hap : a ≠ 0<GOAL>Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Finset.Ico 1 (p / 2).succ).val = Multiset.map (fun a => a) (Finset.Ico 1 (p / 2).succ).val
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑a ^ (p / 2) * ↑(p / 2)! = (-1) ^ (Finset.filter (fun x => ¬(↑a * ↑x).val ≤ p / 2) (Finset.Ico 1 (p / 2).succ)).card * ↑(p / 2)!
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑a ^ (p / 2) = ↑((-1) ^ (Finset.filter (fun x => p / 2 < (↑a * ↑x).val) (Finset.Ico 1 (p / 2).succ)).card)
<VAR>p : ℕ<VAR>h : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hp : p ≠ 2<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p a = (-1) ^ (Finset.filter (fun x => p / 2 < (↑a * ↑x).val) (Finset.Ico 1 (p / 2).succ)).card
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp2 : Fact (p % 2 = 1)<VAR>a : ℕ<VAR>hap : ↑a ≠ 0<GOAL>↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, a * x) = ↑(Finset.filter (fun x => p / 2 < (↑a * ↑x).val) (Finset.Ico 1 (p / 2).succ)).card + ↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, x) + ↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, a * x / p)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Fact (p % 2 = 1)<VAR>a : ℕ<VAR>ha2 : a % 2 = 1<VAR>hap : ↑a ≠ 0<GOAL>(Finset.filter (fun x => p / 2 < (↑a * ↑x).val) (Finset.Ico 1 (p / 2).succ)).card ≡ ∑ x ∈ Finset.Ico 1 (p / 2).succ, x * a / p [MOD 2]
<VAR>a b c : ℕ<VAR>hb0 : 0 < b<VAR>hc : a / b ≤ c<GOAL>a / b = (Finset.filter (fun x => x * b ≤ a) (Finset.Ico 1 c.succ)).card
<VAR>p q : ℕ<GOAL>∑ a ∈ Finset.Ico 1 (p / 2).succ, a * q / p = (Finset.filter (fun x => x.2 * p ≤ x.1 * q) (Finset.Ico 1 (p / 2).succ ×ˢ Finset.Ico 1 (q / 2).succ)).card
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq0 : ↑q ≠ 0<GOAL>∑ a ∈ Finset.Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Finset.Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>a : ℕ<VAR>ha1 : a % 2 = 1<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p ↑a = (-1) ^ ∑ x ∈ Finset.Ico 1 (p / 2).succ, x * a / p
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddMonoid α<VAR>SMul γ α<VAR>self : SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a : α<VAR>z : γ<GOAL>(z • a) ∣[k;γ] g = z • a ∣[k;γ] g
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddMonoid α<VAR>SMul γ α<VAR>self : SlashAction β G α γ<VAR>k : β<VAR>g : G<GOAL>0 ∣[k;γ] g = 0
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddMonoid α<VAR>SMul γ α<VAR>self : SlashAction β G α γ<VAR>k : β<VAR>g h : G<VAR>a : α<GOAL>a ∣[k;γ] (g * h) = (a ∣[k;γ] g) ∣[k;γ] h
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddMonoid α<VAR>SMul γ α<VAR>self : SlashAction β G α γ<VAR>k : β<VAR>a : α<GOAL>a ∣[k;γ] 1 = a
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddMonoid α<VAR>SMul γ α<VAR>self : SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a b : α<GOAL>(a + b) ∣[k;γ] g = a ∣[k;γ] g + b ∣[k;γ] g
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>Group G<VAR>AddGroup α<VAR>SMul γ α<VAR>SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a : α<GOAL>(-a) ∣[k;γ] g = -a ∣[k;γ] g
<VAR>R : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>α : Type u_4<VAR>γ : Type u_5<VAR>Group G<VAR>AddGroup α<VAR>Monoid γ<VAR>MulAction γ α<VAR>SMul R γ<VAR>SMul R α<VAR>IsScalarTower R γ α<VAR>SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a : α<VAR>r : R<GOAL>(r • a) ∣[k;γ] g = r • a ∣[k;γ] g
<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<GOAL>ModularForm.slash k (A * B) f = ModularForm.slash k B (ModularForm.slash k A f)
<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<GOAL>ModularForm.slash k A (f + g) = ModularForm.slash k A f + ModularForm.slash k A g
<VAR>k : ℤ<VAR>f : ℍ → ℂ<GOAL>ModularForm.slash k 1 f = f
<VAR>α : Type u_1<VAR>SMul α ℂ<VAR>IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>c : α<GOAL>ModularForm.slash k A (c • f) = c • ModularForm.slash k A f
<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<GOAL>ModularForm.slash k A 0 = 0
<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>A : ↥GL(2, ℝ)⁺<GOAL>f ∣[k] A = ModularForm.slash k A f
<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>γ : ↥Γ<GOAL>f ∣[k] γ = f ∣[k] ↑↑γ
<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>γ : SL(2, ℤ)<GOAL>f ∣[k] γ = f ∣[k] ↑γ
<VAR>A : SL(2, ℤ)<VAR>x : ℂ<GOAL>Function.const ℍ x ∣[0] A = Function.const ℍ x
<VAR>A : SL(2, ℤ)<GOAL>1 ∣[0] A = 1
<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ℍ → ℂ<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>(f ∣[k] γ) z = f z ↔ f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
<VAR>k1 k2 : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f g : ℍ → ℂ<GOAL>(f * g) ∣[k1 + k2] A = (↑↑A).det • f ∣[k1] A * g ∣[k2] A
<VAR>k1 k2 : ℤ<VAR>A : SL(2, ℤ)<VAR>f g : ℍ → ℂ<GOAL>(f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A
<VAR>k1 k2 : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>A : ↥Γ<VAR>f g : ℍ → ℂ<GOAL>(f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A
<VAR>a : ℤ<GOAL>jacobiSym a 0 = 1
<VAR>a : ℤ<GOAL>jacobiSym a 1 = 1
<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = jacobiSym a p
<VAR>a : ℤ<VAR>b₁ b₂ : ℕ<VAR>hb₁ : b₁ ≠ 0<VAR>hb₂ : b₂ ≠ 0<GOAL>jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
<VAR>a : ℤ<VAR>b₁ b₂ : ℕ<VAR>NeZero b₁<VAR>NeZero b₂<GOAL>jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
<VAR>a : ℤ<VAR>b : ℕ<GOAL>jacobiSym a b = 0 ∨ jacobiSym a b = 1 ∨ jacobiSym a b = -1
<VAR>b : ℕ<GOAL>jacobiSym 1 b = 1
<VAR>a₁ a₂ : ℤ<VAR>b : ℕ<GOAL>jacobiSym (a₁ * a₂) b = jacobiSym a₁ b * jacobiSym a₂ b
<VAR>a : ℤ<VAR>b : ℕ<VAR>NeZero b<GOAL>jacobiSym a b = 0 ↔ a.gcd ↑b ≠ 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>jacobiSym a b ≠ 0
<VAR>a : ℤ<VAR>b : ℕ<GOAL>jacobiSym a b = 0 ↔ b ≠ 0 ∧ a.gcd ↑b ≠ 1
<VAR>b : ℕ<VAR>hb : 1 < b<GOAL>jacobiSym 0 b = 0
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>jacobiSym a b = 1 ∨ jacobiSym a b = -1
<VAR>a : ℤ<VAR>e b : ℕ<GOAL>jacobiSym (a ^ e) b = jacobiSym a b ^ e
<VAR>a : ℤ<VAR>b e : ℕ<GOAL>jacobiSym a (b ^ e) = jacobiSym a b ^ e
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>jacobiSym a b ^ 2 = 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>jacobiSym (a ^ 2) b = 1
<VAR>a : ℤ<VAR>b : ℕ<GOAL>jacobiSym a b = jacobiSym (a % ↑b) b
<VAR>a₁ a₂ : ℤ<VAR>b : ℕ<VAR>h : a₁ % ↑b = a₂ % ↑b<GOAL>jacobiSym a₁ b = jacobiSym a₂ b
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : jacobiSym a p = -1<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x ^ 2 - a * y ^ 2<GOAL>↑p ∣ x ∧ ↑p ∣ y
<VAR>l : List ℤ<VAR>n : ℕ<GOAL>jacobiSym l.prod n = (List.map (fun a => jacobiSym a n) l).prod
<VAR>a : ℤ<VAR>l : List ℕ<VAR>hl : ∀ n ∈ l, n ≠ 0<GOAL>jacobiSym a l.prod = (List.map (fun n => jacobiSym a n) l).prod
<VAR>a : ℤ<VAR>n : ℕ<VAR>h : jacobiSym a n = -1<GOAL>∃ p, Nat.Prime p ∧ p ∣ n ∧ jacobiSym a p = -1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : jacobiSym a b = -1<GOAL>¬IsSquare ↑a
<VAR>a : ℤ<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>jacobiSym a p = -1 ↔ ¬IsSquare ↑a
<VAR>a : ℤ<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>h : jacobiSym a p = 1<GOAL>IsSquare ↑a
<VAR>a : ℤ<VAR>R : Type u_1<VAR>CommSemiring R<VAR>χ : R →* ℤ<VAR>hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym a b = χ ↑b
<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym (-1) b = ZMod.χ₄ ↑b
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym (-a) b = ZMod.χ₄ ↑b * jacobiSym a b
<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym 2 b = ZMod.χ₈ ↑b
<VAR>b : ℕ<VAR>hb : Odd b<GOAL>jacobiSym (-2) b = ZMod.χ₈' ↑b
<VAR>a : ℤ<VAR>b : ℕ<VAR>ha4 : a % 4 = 0<VAR>hb2 : b % 2 = 1<GOAL>jacobiSym (a / 4) b = jacobiSym a b
<VAR>a : ℤ<VAR>b : ℕ<VAR>ha2 : a % 2 = 0<VAR>hb2 : b % 2 = 1<GOAL>(if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (a / 2) b else jacobiSym (a / 2) b) = jacobiSym a b
<VAR>m n₁ n₂ : ℕ<VAR>NeZero n₁<VAR>NeZero n₂<GOAL>qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>jacobiSym (↑a) b = qrSign b a * jacobiSym (↑b) a