ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>h : NumberField.mixedEmbedding.minkowskiBound K 1 < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)<GOAL>∃ a, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < ↑(f w)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>w₀ : { w // w.IsComplex }<VAR>h : NumberField.mixedEmbedding.minkowskiBound K 1 < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀)<GOAL>∃ a, a ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧ |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₀ : NumberField.InfinitePlace K<VAR>hw₀ : w₀.IsReal<VAR>B : NNReal<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < ↑(max B 1)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₀ : NumberField.InfinitePlace K<VAR>hw₀ : w₀.IsComplex<VAR>B : NNReal<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑B<GOAL>∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>B : ℝ<VAR>h : NumberField.mixedEmbedding.minkowskiBound K I ≤ MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(FiniteDimensional.finrank ℚ K)) ^ FiniteDimensional.finrank ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<VAR>h : NumberField.mixedEmbedding.minkowskiBound K 1 ≤ MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B)<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(FiniteDimensional.finrank ℚ K)) ^ FiniteDimensional.finrank ℚ K
<VAR>k G : Type u<VAR>Field k<VAR>Monoid G<VAR>V W : FDRep k G<VAR>i : V ≅ W<VAR>g : G<GOAL>W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g)
<VAR>k G : Type u<VAR>Field k<VAR>Monoid G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module k V<VAR>FiniteDimensional k V<VAR>ρ : Representation k G V<GOAL>(FDRep.of ρ).ρ = ρ
<VAR>k G : Type u<VAR>Field k<VAR>Monoid G<VAR>V : FDRep k G<GOAL>((CategoryTheory.forget₂ (FDRep k G) (Rep k G)).obj V).ρ = V.ρ
<VAR>k G : Type u<VAR>Field k<VAR>Monoid G<VAR>IsAlgClosed k<VAR>V W : FDRep k G<VAR>CategoryTheory.Simple V<VAR>CategoryTheory.Simple W<GOAL>FiniteDimensional.finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0
<VAR>k G V : Type u<VAR>Field k<VAR>Group G<VAR>AddCommGroup V<VAR>Module k V<VAR>FiniteDimensional k V<VAR>ρV : Representation k G V<VAR>W : FDRep k G<GOAL>(FDRep.dualTensorIsoLinHom ρV W).hom.hom = dualTensorHom k V (CoeSort.coe W)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<GOAL>groupCohomology.Hilbert90.aux f ≠ 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>hf : groupCohomology.IsMulOneCocycle f<GOAL>groupCohomology.IsMulOneCoboundary f
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Monoid G<VAR>V : FDRep k G<VAR>g h : G<GOAL>V.character (h * g) = V.character (g * h)
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Monoid G<VAR>V : FDRep k G<GOAL>V.character 1 = ↑(FiniteDimensional.finrank k (CoeSort.coe V))
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Monoid G<VAR>V W : FDRep k G<GOAL>(V ⊗ W).character = V.character * W.character
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Monoid G<VAR>V W : FDRep k G<GOAL>FDRep.character (Action.FunctorCategoryEquivalence.inverse.obj (Action.FunctorCategoryEquivalence.functor.obj V ⊗ Action.FunctorCategoryEquivalence.functor.obj W)) = V.character * W.character
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Monoid G<VAR>V W : FDRep k G<VAR>i : V ≅ W<GOAL>V.character = W.character
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Group G<VAR>V : FDRep k G<VAR>g h : G<GOAL>V.character (h * g * h⁻¹) = V.character g
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Group G<VAR>V : FDRep k G<VAR>g : G<GOAL>(FDRep.of (Representation.dual V.ρ)).character g = V.character g⁻¹
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Group G<VAR>V W : FDRep k G<VAR>g : G<GOAL>(FDRep.of (Representation.linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Group G<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>V : FDRep k G<GOAL>⅟↑(Fintype.card G) • ∑ g : G, V.character g = ↑(FiniteDimensional.finrank k ↥(Representation.invariants V.ρ))
<VAR>k : Type u<VAR>Field k<VAR>G : Grp<VAR>IsAlgClosed k<VAR>Fintype ↑G<VAR>Invertible ↑(Fintype.card ↑G)<VAR>V W : FDRep k ↑G<VAR>CategoryTheory.Simple V<VAR>CategoryTheory.Simple W<GOAL>⅟↑(Fintype.card ↑G) • ∑ g : ↑G, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
<VAR>d : ℤ<VAR>n : ℤ<GOAL>(Zsqrtd.ofInt n).re = n
<VAR>d : ℤ<VAR>n : ℤ<GOAL>(Zsqrtd.ofInt n).im = 0
<VAR>d : ℤ<GOAL>Zsqrtd.re 0 = 0
<VAR>d : ℤ<GOAL>Zsqrtd.im 0 = 0
<VAR>d : ℤ<GOAL>Zsqrtd.re 1 = 1
<VAR>d : ℤ<GOAL>Zsqrtd.im 1 = 0
<VAR>d : ℤ<GOAL>Zsqrtd.sqrtd.re = 0
<VAR>d : ℤ<GOAL>Zsqrtd.sqrtd.im = 1
<VAR>d : ℤ<VAR>x y x' y' : ℤ<GOAL>{ re := x, im := y } + { re := x', im := y' } = { re := x + x', im := y + y' }
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z + w).re = z.re + w.re
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z + w).im = z.im + w.im
<VAR>d : ℤ<VAR>z : ℤ√d<GOAL>(-z).re = -z.re
<VAR>d : ℤ<VAR>z : ℤ√d<GOAL>(-z).im = -z.im
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z * w).re = z.re * w.re + d * z.im * w.im
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z * w).im = z.re * w.im + z.im * w.re
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z - w).re = z.re - w.re
<VAR>d : ℤ<VAR>z w : ℤ√d<GOAL>(z - w).im = z.im - w.im
<VAR>d : ℤ<VAR>x y : ℤ<GOAL>star { re := x, im := y } = { re := x, im := -y }
<VAR>d : ℤ<VAR>z : ℤ√d<GOAL>(star z).re = z.re
<VAR>d : ℤ<VAR>z : ℤ√d<GOAL>(star z).im = -z.im
<VAR>d : ℤ<VAR>n : ℕ<GOAL>(↑n).re = ↑n
<VAR>d : ℤ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).re = ↑n
<VAR>d : ℤ<VAR>n : ℕ<GOAL>(↑n).im = 0
<VAR>d : ℤ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).im = 0
<VAR>d : ℤ<VAR>n : ℕ<GOAL>↑n = { re := ↑n, im := 0 }
<VAR>d : ℤ<VAR>n : ℤ<GOAL>(↑n).re = n
<VAR>d : ℤ<VAR>n : ℤ<GOAL>(↑n).im = 0
<VAR>d : ℤ<VAR>n : ℤ<GOAL>↑n = { re := n, im := 0 }
<VAR>d : ℤ<VAR>n : ℤ<GOAL>Zsqrtd.ofInt n = ↑n
<VAR>d : ℤ<VAR>n x y : ℤ<GOAL>↑n * { re := x, im := y } = { re := n * x, im := n * y }
<VAR>d : ℤ<VAR>a : ℤ<VAR>b : ℤ√d<GOAL>(↑a * b).re = a * b.re
<VAR>d : ℤ<VAR>a : ℤ<VAR>b : ℤ√d<GOAL>(↑a * b).im = a * b.im
<VAR>d : ℤ<VAR>x y : ℤ<GOAL>Zsqrtd.sqrtd * { re := x, im := y } = { re := d * y, im := x }
<VAR>d : ℤ<GOAL>Zsqrtd.sqrtd * Zsqrtd.sqrtd = ↑d
<VAR>d : ℤ<VAR>n x y : ℤ<GOAL>Zsqrtd.sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }
<VAR>d x y : ℤ<GOAL>{ re := x, im := y } = ↑x + Zsqrtd.sqrtd * ↑y
<VAR>d : ℤ<VAR>z : ℤ<VAR>a : ℤ√d<GOAL>↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
<VAR>d : ℤ<VAR>a b : ℤ<GOAL>↑a ∣ ↑b ↔ a ∣ b
<VAR>d a : ℤ<VAR>b c : ℤ√d<VAR>ha : a ≠ 0<VAR>h : ↑a * b = ↑a * c<GOAL>b = c
<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>0 < a.re.gcd a.im ↔ a ≠ 0
<VAR>c d x y z w : ℕ<VAR>xz : z ≤ x<VAR>yw : y ≤ w<VAR>xy : Zsqrtd.SqLe x c y d<GOAL>Zsqrtd.SqLe z c w d
<VAR>c d x y z w : ℕ<VAR>xy : Zsqrtd.SqLe x c y d<VAR>zw : Zsqrtd.SqLe z c w d<GOAL>c * (x * z) ≤ d * (y * w)
<VAR>c d x y z w : ℕ<VAR>xy : Zsqrtd.SqLe x c y d<VAR>zw : Zsqrtd.SqLe z c w d<GOAL>Zsqrtd.SqLe (x + z) c (y + w) d
<VAR>c d x y z w : ℕ<VAR>zw : Zsqrtd.SqLe y d x c<VAR>h : Zsqrtd.SqLe (x + z) c (y + w) d<GOAL>Zsqrtd.SqLe z c w d
<VAR>c d x y : ℕ<VAR>n : ℕ<VAR>xy : Zsqrtd.SqLe x c y d<GOAL>Zsqrtd.SqLe (n * x) c (n * y) d
<VAR>d x y z w : ℕ<GOAL>(Zsqrtd.SqLe x 1 y d → Zsqrtd.SqLe z 1 w d → Zsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧ (Zsqrtd.SqLe x 1 y d → Zsqrtd.SqLe w d z 1 → Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧ (Zsqrtd.SqLe y d x 1 → Zsqrtd.SqLe z 1 w d → Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧ (Zsqrtd.SqLe y d x 1 → Zsqrtd.SqLe w d z 1 → Zsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1)
<VAR>c d : ℕ<VAR>x y : ℤ<GOAL>Zsqrtd.Nonnegg c d x y = Zsqrtd.Nonnegg d c y x
<VAR>c d a b : ℕ<GOAL>Zsqrtd.Nonnegg c d (-↑a) ↑b ↔ Zsqrtd.SqLe a d b c
<VAR>c d a b : ℕ<GOAL>Zsqrtd.Nonnegg c d (↑a) (-↑b) ↔ Zsqrtd.SqLe b c a d
<VAR>c d a : ℕ<VAR>b : ℤ<GOAL>(∀ (x : ℕ), b = -↑x → Zsqrtd.SqLe x c a d) → Zsqrtd.Nonnegg c d (↑a) b
<VAR>c d b : ℕ<VAR>a : ℤ<VAR>h : ∀ (x : ℕ), a = -↑x → Zsqrtd.SqLe x d b c<GOAL>Zsqrtd.Nonnegg c d a ↑b
<VAR>d : ℤ<VAR>n : ℤ√d<GOAL>n.norm = n.re * n.re - d * n.im * n.im
<VAR>d : ℤ<GOAL>Zsqrtd.norm 0 = 0
<VAR>d : ℤ<GOAL>Zsqrtd.norm 1 = 1
<VAR>d : ℤ<VAR>n : ℤ<GOAL>(↑n).norm = n * n
<VAR>d : ℤ<VAR>n : ℕ<GOAL>(↑n).norm = ↑n * ↑n
<VAR>d : ℤ<VAR>n m : ℤ√d<GOAL>(n * m).norm = n.norm * m.norm
<VAR>d : ℤ<VAR>x : ℤ√d<GOAL>(-x).norm = x.norm
<VAR>d : ℤ<VAR>x : ℤ√d<GOAL>(star x).norm = x.norm
<VAR>d : ℤ<VAR>hd : d ≤ 0<VAR>n : ℤ√d<GOAL>0 ≤ n.norm
<VAR>d : ℤ<VAR>x : ℤ√d<GOAL>x.norm.natAbs = 1 ↔ IsUnit x
<VAR>d : ℤ<VAR>z : ℤ√d<GOAL>IsUnit z ↔ IsUnit z.norm
<VAR>d : ℤ<VAR>hd : d ≤ 0<VAR>z : ℤ√d<GOAL>z.norm = 1 ↔ IsUnit z
<VAR>d : ℤ<VAR>hd : d < 0<VAR>z : ℤ√d<GOAL>z.norm = 0 ↔ z = 0
<VAR>d : ℤ<VAR>hd : d ≤ 0<VAR>x y : ℤ√d<VAR>h : Associated x y<GOAL>x.norm = y.norm
<VAR>d : ℕ<VAR>a : ℤ√↑d<GOAL>a.Nonneg → ∃ x y, a = { re := ↑x, im := ↑y } ∨ a = { re := ↑x, im := -↑y } ∨ a = { re := -↑x, im := ↑y }
<VAR>d : ℕ<VAR>a : ℤ√↑d<GOAL>a.Nonneg ↔ 0 ≤ a
<VAR>d : ℕ<VAR>x y z w : ℤ<VAR>xz : x ≤ z<VAR>yw : y ≤ w<GOAL>{ re := x, im := y } ≤ { re := z, im := w }
<VAR>d : ℕ<VAR>a : ℤ√↑d<GOAL>a.Nonneg ∨ (-a).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ab : a ≤ b<VAR>c : ℤ√↑d<GOAL>c + a ≤ c + b
<VAR>d : ℕ<VAR>a b c : ℤ√↑d<VAR>h : c + a ≤ c + b<GOAL>a ≤ b
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>h : a < b<VAR>c : ℤ√↑d<GOAL>c + a < c + b
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>ha : a.Nonneg<GOAL>(Zsqrtd.sqrtd * a).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha : a.Nonneg<VAR>hb : b.Nonneg<GOAL>(a * b).Nonneg
<VAR>c d y : ℕ<VAR>h : 0 < c<GOAL>¬Zsqrtd.SqLe (y + 1) c 0 d
<VAR>x : ℕ<VAR>self : Zsqrtd.Nonsquare x<VAR>n : ℕ<GOAL>x ≠ n * n
<VAR>x : ℕ<VAR>Zsqrtd.Nonsquare x<VAR>n : ℕ<GOAL>x ≠ n * n
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<GOAL>0 < d
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>x y : ℕ<VAR>h : x * x = d * y * y<GOAL>x = 0 ∧ y = 0
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>x y : ℤ<VAR>h : x * x = ↑d * y * y<GOAL>x = 0 ∧ y = 0
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>x y : ℕ<GOAL>(x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1)
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>a : ℤ√↑d<GOAL>a.Nonneg → (-a).Nonneg → a = 0
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>a b : ℤ√↑d<VAR>ab : a ≤ b<VAR>ba : b ≤ a<GOAL>a = b
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>a b : ℤ√↑d<GOAL>a * b = 0 → a = 0 ∨ b = 0
<VAR>d : ℕ<VAR>dnsq : Zsqrtd.Nonsquare d<VAR>a b : ℤ√↑d<VAR>a0 : 0 < a<VAR>b0 : 0 < b<GOAL>0 < a * b
<VAR>R : Type<VAR>Ring R<VAR>d : ℤ<VAR>f g : ℤ√d →+* R<VAR>h : f Zsqrtd.sqrtd = g Zsqrtd.sqrtd<GOAL>f = g
<VAR>R : Type<VAR>CommRing R<VAR>d : ℤ<VAR>f : ℤ√d →+* R<GOAL>↑(Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd
<VAR>R : Type<VAR>CommRing R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>a : ℤ√d<GOAL>(Zsqrtd.lift r) a = ↑a.re + ↑a.im * ↑r
<VAR>R : Type<VAR>CommRing R<VAR>CharZero R<VAR>d : ℤ<VAR>r : { r // r * r = ↑d }<VAR>hd : ∀ (n : ℤ), d ≠ n * n<GOAL>Function.Injective ⇑(Zsqrtd.lift r)
<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>a.norm = 1 ↔ a ∈ unitary (ℤ√d)
<VAR>d : ℤ<GOAL>MonoidHom.mker Zsqrtd.normMonoidHom = unitary (ℤ√d)
<VAR>R : Type u_1<VAR>Zero R<VAR>f : ArithmeticFunction R<GOAL>f.toFun = ⇑f
<VAR>R : Type u_1<VAR>Zero R<VAR>f : ℕ → R<VAR>hf : f 0 = 0<GOAL>⇑{ toFun := f, map_zero' := hf } = f
<VAR>R : Type u_1<VAR>Zero R<VAR>f : ArithmeticFunction R<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>Zero R<VAR>f g : ArithmeticFunction R<GOAL>⇑f = ⇑g ↔ f = g
<VAR>R : Type u_1<VAR>Zero R<VAR>x : ℕ<GOAL>0 x = 0
<VAR>R : Type u_1<VAR>Zero R<VAR>f g : ArithmeticFunction R<VAR>h : ∀ (x : ℕ), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>Zero R<VAR>f g : ArithmeticFunction R<GOAL>f = g ↔ ∀ (x : ℕ), f x = g x
<VAR>R : Type u_1<VAR>Zero R<VAR>One R<VAR>x : ℕ<GOAL>1 x = if x = 1 then 1 else 0
<VAR>R : Type u_1<VAR>Zero R<VAR>One R<GOAL>1 1 = 1
<VAR>R : Type u_1<VAR>Zero R<VAR>One R<VAR>x : ℕ<VAR>h : x ≠ 1<GOAL>1 x = 0
<VAR>f : ArithmeticFunction ℕ<GOAL>↑f = f
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>f : ArithmeticFunction ℕ<VAR>x : ℕ<GOAL>↑f x = ↑(f x)
<VAR>f : ArithmeticFunction ℤ<GOAL>↑f = f
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>f : ArithmeticFunction ℤ<VAR>x : ℕ<GOAL>↑f x = ↑(f x)
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>f : ArithmeticFunction ℕ<GOAL>↑↑f = ↑f
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>AddGroupWithOne R<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>f g : ArithmeticFunction R<VAR>n : ℕ<GOAL>(f + g) n = f n + g n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Zero R<VAR>AddCommMonoid M<VAR>SMul R M<VAR>f : ArithmeticFunction R<VAR>g : ArithmeticFunction M<VAR>n : ℕ<GOAL>(f • g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 • g x.2
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ArithmeticFunction R<VAR>n : ℕ<GOAL>(f * g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ArithmeticFunction R<GOAL>(f * g) 1 = f 1 * g 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ArithmeticFunction ℕ<GOAL>↑(f * g) = ↑f * ↑g
<VAR>R : Type u_1<VAR>Ring R<VAR>f g : ArithmeticFunction ℤ<GOAL>↑(f * g) = ↑f * ↑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : ArithmeticFunction R<VAR>h : ArithmeticFunction M<GOAL>(f * g) • h = f • g • h
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : ArithmeticFunction M<GOAL>1 • b = b
<VAR>x : ℕ<GOAL>ArithmeticFunction.zeta x = if x = 0 then 0 else 1
<VAR>x : ℕ<VAR>h : x ≠ 0<GOAL>ArithmeticFunction.zeta x = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : ArithmeticFunction M<VAR>x : ℕ<GOAL>(↑ArithmeticFunction.zeta • f) x = ∑ i ∈ x.divisors, f i
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>(↑ArithmeticFunction.zeta * f) x = ∑ i ∈ x.divisors, f i
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>(f * ↑ArithmeticFunction.zeta) x = ∑ i ∈ x.divisors, f i
<VAR>f : ArithmeticFunction ℕ<VAR>x : ℕ<GOAL>(ArithmeticFunction.zeta * f) x = ∑ i ∈ x.divisors, f i
<VAR>f : ArithmeticFunction ℕ<VAR>x : ℕ<GOAL>(f * ArithmeticFunction.zeta) x = ∑ i ∈ x.divisors, f i
<VAR>R : Type u_1<VAR>MulZeroClass R<VAR>f g : ArithmeticFunction R<VAR>x : ℕ<GOAL>(f.pmul g) x = f x * g x
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f g : ArithmeticFunction R<GOAL>f.pmul g = g.pmul f
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f₁ f₂ f₃ : ArithmeticFunction R<GOAL>(f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : ArithmeticFunction R<GOAL>f.pmul ↑ArithmeticFunction.zeta = f
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : ArithmeticFunction R<GOAL>(↑ArithmeticFunction.zeta).pmul f = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<GOAL>f.ppow 0 = ↑ArithmeticFunction.zeta
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<VAR>k x : ℕ<VAR>kpos : 0 < k<GOAL>(f.ppow k) x = f x ^ k
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<VAR>k : ℕ<GOAL>f.ppow (k + 1) = f.pmul (f.ppow k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : ArithmeticFunction R<VAR>k : ℕ<VAR>kpos : 0 < k<GOAL>f.ppow (k + 1) = (f.ppow k).pmul f
<VAR>R : Type u_1<VAR>GroupWithZero R<VAR>f g : ArithmeticFunction R<VAR>n : ℕ<GOAL>(f.pdiv g) n = f n / g n
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>f : ArithmeticFunction R<GOAL>f.pdiv ↑ArithmeticFunction.zeta = f
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f : ℕ → R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(ArithmeticFunction.prodPrimeFactors fun p => f p) n = ∏ p ∈ n.primeFactors, f p
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>h : f.IsMultiplicative<GOAL>f 1 = 1
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>m n : ℕ<VAR>h : m.Coprime n<GOAL>f (m * n) = f m * f n
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommMonoidWithZero R<VAR>g : ι → ℕ<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>s : Finset ι<VAR>hs : (↑s).Pairwise (Nat.Coprime on g)<GOAL>f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : ArithmeticFunction R<VAR>h_mult : f.IsMultiplicative<VAR>t : Finset ℕ<VAR>ht : ∀ p ∈ t, Nat.Prime p<GOAL>f (∏ a ∈ t, a) = ∏ a ∈ t, f a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : ArithmeticFunction R<VAR>h_mult : f.IsMultiplicative<VAR>l : ℕ<VAR>t : Finset ℕ<VAR>ht : t ⊆ l.primeFactors<GOAL>f (∏ a ∈ t, a) = ∏ a ∈ t, f a
<VAR>R : Type u_1<VAR>f : ArithmeticFunction ℕ<VAR>Semiring R<VAR>h : f.IsMultiplicative<GOAL>(↑f).IsMultiplicative
<VAR>R : Type u_1<VAR>f : ArithmeticFunction ℤ<VAR>Ring R<VAR>h : f.IsMultiplicative<GOAL>(↑f).IsMultiplicative
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>(f * g).IsMultiplicative
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>(f.pmul g).IsMultiplicative
<VAR>R : Type u_1<VAR>CommGroupWithZero R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>(f.pdiv g).IsMultiplicative
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>f n = n.factorization.prod fun p k => f (p ^ k)
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>f : ArithmeticFunction R<GOAL>f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>g : ArithmeticFunction R<VAR>hg : g.IsMultiplicative<GOAL>f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f : ℕ → R<GOAL>(ArithmeticFunction.prodPrimeFactors f).IsMultiplicative
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>(ArithmeticFunction.prodPrimeFactors fun p => (f + g) p) n = (f * g) n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<GOAL>f (x.lcm y) * f (x.gcd y) = f x * f y
<VAR>x : ℕ<GOAL>ArithmeticFunction.id x = x
<VAR>k n : ℕ<GOAL>(ArithmeticFunction.pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k
<GOAL>ArithmeticFunction.pow 0 = ArithmeticFunction.zeta
<VAR>k n : ℕ<GOAL>(ArithmeticFunction.sigma k) n = ∑ d ∈ n.divisors, d ^ k
<VAR>k p i : ℕ<VAR>hp : Nat.Prime p<GOAL>(ArithmeticFunction.sigma k) (p ^ i) = ∑ j ∈ Finset.range (i + 1), p ^ (j * k)
<VAR>n : ℕ<GOAL>(ArithmeticFunction.sigma 1) n = ∑ d ∈ n.divisors, d
<VAR>p i : ℕ<VAR>hp : Nat.Prime p<GOAL>(ArithmeticFunction.sigma 1) (p ^ i) = ∑ k ∈ Finset.range (i + 1), p ^ k
<VAR>n : ℕ<GOAL>(ArithmeticFunction.sigma 0) n = n.divisors.card
<VAR>p i : ℕ<VAR>hp : Nat.Prime p<GOAL>(ArithmeticFunction.sigma 0) (p ^ i) = i + 1
<VAR>k : ℕ<GOAL>ArithmeticFunction.zeta * ArithmeticFunction.pow k = ArithmeticFunction.sigma k
<VAR>R : Type u_1<VAR>MonoidWithZero R<GOAL>ArithmeticFunction.IsMultiplicative 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>k : ℕ<GOAL>(f.ppow k).IsMultiplicative
<VAR>k : ℕ<GOAL>(ArithmeticFunction.pow k).IsMultiplicative
<VAR>k : ℕ<GOAL>(ArithmeticFunction.sigma k).IsMultiplicative
<VAR>n : ℕ<GOAL>ArithmeticFunction.cardFactors n = n.primeFactorsList.length
<VAR>n : ℕ<GOAL>ArithmeticFunction.cardFactors n = 1 ↔ Nat.Prime n
<VAR>m n : ℕ<VAR>m0 : m ≠ 0<VAR>n0 : n ≠ 0<GOAL>ArithmeticFunction.cardFactors (m * n) = ArithmeticFunction.cardFactors m + ArithmeticFunction.cardFactors n
<VAR>s : Multiset ℕ<VAR>h0 : s.prod ≠ 0<GOAL>ArithmeticFunction.cardFactors s.prod = (Multiset.map (⇑ArithmeticFunction.cardFactors) s).sum
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>ArithmeticFunction.cardFactors p = 1
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<GOAL>ArithmeticFunction.cardFactors (p ^ k) = k
<GOAL>ArithmeticFunction.cardDistinctFactors 0 = 0
<GOAL>ArithmeticFunction.cardDistinctFactors 1 = 0
<VAR>n : ℕ<GOAL>ArithmeticFunction.cardDistinctFactors n = n.primeFactorsList.dedup.length
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>ArithmeticFunction.cardDistinctFactors n = ArithmeticFunction.cardFactors n ↔ Squarefree n
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<GOAL>ArithmeticFunction.cardDistinctFactors (p ^ k) = 1
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>ArithmeticFunction.cardDistinctFactors p = 1
<VAR>n : ℕ<VAR>h : Squarefree n<GOAL>ArithmeticFunction.moebius n = (-1) ^ ArithmeticFunction.cardFactors n
<VAR>n : ℕ<VAR>h : ¬Squarefree n<GOAL>ArithmeticFunction.moebius n = 0
<VAR>n : ℕ<GOAL>ArithmeticFunction.moebius n ≠ 0 ↔ Squarefree n
<VAR>n : ℕ<GOAL>ArithmeticFunction.moebius n = 0 ∨ ArithmeticFunction.moebius n = 1 ∨ ArithmeticFunction.moebius n = -1
<VAR>n : ℕ<GOAL>ArithmeticFunction.moebius n ≠ 0 ↔ ArithmeticFunction.moebius n = 1 ∨ ArithmeticFunction.moebius n = -1
<VAR>l : ℕ<VAR>hl : Squarefree l<GOAL>ArithmeticFunction.moebius l ^ 2 = 1
<VAR>l : ℕ<VAR>hl : Squarefree l<GOAL>|ArithmeticFunction.moebius l| = 1
<VAR>n : ℕ<GOAL>ArithmeticFunction.moebius n ^ 2 = if Squarefree n then 1 else 0
<VAR>n : ℕ<GOAL>|ArithmeticFunction.moebius n| = if Squarefree n then 1 else 0
<VAR>n : ℕ<GOAL>|ArithmeticFunction.moebius n| ≤ 1
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>ArithmeticFunction.moebius p = -1
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<GOAL>ArithmeticFunction.moebius (p ^ k) = if k = 1 then -1 else 0
<VAR>n : ℕ<VAR>hn : IsPrimePow n<VAR>hn' : ¬Nat.Prime n<GOAL>ArithmeticFunction.moebius n = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : ArithmeticFunction R<VAR>h_mult : f.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) * f d
<GOAL>ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
<GOAL>↑ArithmeticFunction.zeta * ArithmeticFunction.moebius = 1
<VAR>R : Type u_1<VAR>Ring R<GOAL>↑ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
<VAR>R : Type u_1<VAR>Ring R<GOAL>↑ArithmeticFunction.zeta * ↑ArithmeticFunction.moebius = 1
<VAR>R : Type u_1<VAR>CommRing R<GOAL>↑ArithmeticFunction.zetaUnit = ↑ArithmeticFunction.zeta
<VAR>R : Type u_1<VAR>CommRing R<GOAL>↑ArithmeticFunction.zetaUnit⁻¹ = ↑ArithmeticFunction.moebius
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n
<VAR>R : Type u_1<VAR>Ring R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>CommGroup R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n
<VAR>R : Type u_1<VAR>CommGroupWithZero R<VAR>f g : ℕ → R<VAR>hf : ∀ (n : ℕ), 0 < n → f n ≠ 0<VAR>hg : ∀ (n : ℕ), 0 < n → g n ≠ 0<GOAL>(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>(∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>hs₀ : 0 ∉ s<GOAL>(∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n