ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>DecidablePred fun n => p n ≠ 0<VAR>hp : ∃ n, p n ≠ 0<GOAL>p.order = Nat.find hp
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>DecidablePred fun n => p n ≠ 0<VAR>hp : p ≠ 0<GOAL>p.order = Nat.find ⋯
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : p ≠ 0<GOAL>p.order = 0 ↔ p 0 ≠ 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : p ≠ 0<GOAL>p p.order ≠ 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : p.order ≠ 0<GOAL>p p.order ≠ 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>Ring 𝕜<VAR>n : ℕ<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousConstSMul 𝕜 E<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : n < p.order<GOAL>p n = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<VAR>y : Fin n → 𝕜<GOAL>(p n) y = (∏ i : Fin n, y i) • p.coeff n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>p.coeff n = 0 ↔ p n = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<VAR>z : 𝕜<GOAL>((p n) fun x => z) = z ^ n • p.coeff n
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>‖p n‖ = ‖p.coeff n‖
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>p.fslope.coeff n = p.coeff (n + 1)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>k n : ℕ<GOAL>(FormalMultilinearSeries.fslope^[k] p).coeff n = p.coeff (n + k)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>c : F<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>constFormalMultilinearSeries 𝕜 E c n = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<GOAL>constFormalMultilinearSeries 𝕜 E 0 = 0
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>f.fpowerSeries x 0 = ContinuousMultilinearMap.curry0 𝕜 E (f x)
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<VAR>n : ℕ<GOAL>f.fpowerSeries x (n + 2) = 0
<VAR>p : ℚ[X]<GOAL>Fact (Polynomial.Splits (algebraMap ℚ ℂ) p)
<VAR>p : ℚ[X]<GOAL>(p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + ((Polynomial.Gal.galActionHom p ℂ) ((Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2<GOAL>Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<GOAL>Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (Polynomial.aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>(Polynomial.X - Polynomial.C ((starRingEnd ℂ) z)) * (Polynomial.X - Polynomial.C z) ∣ Polynomial.map (algebraMap ℝ ℂ) p
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (Polynomial.aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>Polynomial.X ^ 2 - Polynomial.C (2 * z.re) * Polynomial.X + Polynomial.C (‖z‖ ^ 2) ∣ p
<VAR>p : ℝ[X]<VAR>hp : Irreducible p<GOAL>p.natDegree ≤ 2
<VAR>z : ℂ<GOAL>‖z‖ = Complex.abs z
<VAR>t : ℝ<GOAL>‖Complex.exp (↑t * Complex.I)‖ = 1
<VAR>z w : ℂ<GOAL>dist z w = Complex.abs (z - w)
<VAR>z w : ℂ<GOAL>dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
<VAR>x₁ y₁ x₂ y₂ : ℝ<GOAL>dist { re := x₁, im := y₁ } { re := x₂, im := y₂ } = √((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
<VAR>z w : ℂ<VAR>h : z.re = w.re<GOAL>dist z w = dist z.im w.im
<VAR>z w : ℂ<VAR>h : z.re = w.re<GOAL>nndist z w = nndist z.im w.im
<VAR>z w : ℂ<VAR>h : z.re = w.re<GOAL>edist z w = edist z.im w.im
<VAR>z w : ℂ<VAR>h : z.im = w.im<GOAL>dist z w = dist z.re w.re
<VAR>z w : ℂ<VAR>h : z.im = w.im<GOAL>nndist z w = nndist z.re w.re
<VAR>z w : ℂ<VAR>h : z.im = w.im<GOAL>edist z w = edist z.re w.re
<VAR>z : ℂ<GOAL>dist ((starRingEnd ℂ) z) z = 2 * |z.im|
<VAR>z : ℂ<GOAL>nndist ((starRingEnd ℂ) z) z = 2 * Real.nnabs z.im
<VAR>z : ℂ<GOAL>dist z ((starRingEnd ℂ) z) = 2 * |z.im|
<VAR>z : ℂ<GOAL>nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im
<GOAL>Filter.comap (⇑Complex.abs) (nhds 0) = nhds 0
<VAR>r : ℝ<GOAL>‖↑r‖ = ‖r‖
<VAR>r : ℚ<GOAL>‖↑r‖ = |↑r|
<VAR>n : ℤ<GOAL>‖↑n‖ = |↑n|
<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>‖↑n‖ = ↑n
<VAR>z : ℂ<GOAL>Complex.normSq z = ‖z‖ ^ 2
<VAR>r : ℝ<GOAL>‖↑r‖₊ = ‖r‖₊
<VAR>n : ℤ<GOAL>‖↑n‖₊ = ‖n‖₊
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>h : ζ ^ n = 1<VAR>hn : n ≠ 0<GOAL>‖ζ‖₊ = 1
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>h : ζ ^ n = 1<VAR>hn : n ≠ 0<GOAL>‖ζ‖ = 1
<VAR>ι : Type u_2<VAR>a b : ℝ<VAR>f : ι → ℂ<VAR>s : Finset ι<VAR>ha₀ : 0 ≤ a<VAR>ha : ↑a = ∑ i ∈ s, f i<VAR>hb : ↑b = ∑ i ∈ s, ↑‖f i‖<GOAL>a ≤ b
<VAR>z : ℂ<GOAL>‖Complex.equivRealProd z‖ ≤ Complex.abs z
<VAR>z : ℂ<GOAL>‖Complex.equivRealProd z‖ ≤ 1 * Complex.abs z
<GOAL>LipschitzWith 1 ⇑Complex.equivRealProd
<GOAL>AntilipschitzWith (NNReal.sqrt 2) ⇑Complex.equivRealProd
<GOAL>UniformEmbedding ⇑Complex.equivRealProd
<GOAL>∀ (a : ℝ × ℝ), (Complex.equivRealProdCLM.symm a).im = a.2
<GOAL>∀ (a : ℂ), Complex.equivRealProdCLM a = (a.re, a.im)
<GOAL>∀ (a : ℝ × ℝ), (Complex.equivRealProdCLM.symm a).re = a.1
<VAR>p : ℝ × ℝ<GOAL>Complex.equivRealProdCLM.symm p = ↑p.1 + ↑p.2 * Complex.I
<GOAL>Filter.Tendsto (⇑Complex.abs) (Filter.cocompact ℂ) Filter.atTop
<GOAL>Filter.Tendsto (⇑Complex.normSq) (Filter.cocompact ℂ) Filter.atTop
<VAR>z : ℂ<GOAL>Complex.reCLM z = z.re
<VAR>z : ℂ<GOAL>Complex.imCLM z = z.im
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>x : E<GOAL>ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = Complex.reCLM.smulRight x + Complex.I • Complex.imCLM.smulRight x
<VAR>x : ℂ<GOAL>ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = x • 1
<VAR>z : ℂ<GOAL>Complex.conjLIE z = (starRingEnd ℂ) z
<GOAL>Isometry ⇑(starRingEnd ℂ)
<VAR>z w : ℂ<GOAL>dist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = dist z w
<VAR>z w : ℂ<GOAL>nndist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = nndist z w
<VAR>z w : ℂ<GOAL>dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)
<VAR>z w : ℂ<GOAL>nndist ((starRingEnd ℂ) z) w = nndist z ((starRingEnd ℂ) w)
<VAR>f : ℂ →+* ℂ<VAR>hf : Continuous ⇑f<GOAL>f = RingHom.id ℂ ∨ f = starRingEnd ℂ
<GOAL>Complex.conjCLE.toLinearEquiv = Complex.conjAe.toLinearEquiv
<VAR>z : ℂ<GOAL>Complex.conjCLE z = (starRingEnd ℂ) z
<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : α → ℝ<VAR>x : ℝ<VAR>hf : Filter.Tendsto f l (nhds x)<GOAL>Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x)
<VAR>f : ℝ →+* ℂ<VAR>h : Continuous ⇑f<GOAL>f = Complex.ofReal
<GOAL>↑Complex.ofRealCLM = Complex.ofRealAm.toLinearMap
<VAR>x : ℝ<GOAL>Complex.ofRealCLM x = ↑x
<VAR>z : ℂ<GOAL>z * (starRingEnd ℂ) z = ↑‖z‖ ^ 2
<VAR>z : ℂ<GOAL>(starRingEnd ℂ) z * z = ↑‖z‖ ^ 2
<VAR>z : ℂ<VAR>hz : ‖z‖ = 1<GOAL>z⁻¹ = (starRingEnd ℂ) z
<VAR>z : ℂ<GOAL>∃ c, ‖c‖ = 1 ∧ ↑‖z‖ = c * z
<VAR>z : ℂ<GOAL>∃ c, ‖c‖ = 1 ∧ c * ↑‖z‖ = z
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x : ℂ<GOAL>(RCLike.complexRingEquiv h).symm x = ↑x.re + ↑x.im * RCLike.I
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x : 𝕜<GOAL>(RCLike.complexRingEquiv h) x = ↑(RCLike.re x) + ↑(RCLike.im x) * Complex.I
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<GOAL>∀ (a : 𝕜), (RCLike.complexLinearIsometryEquiv h) a = (RCLike.complexRingEquiv h).toFun a
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<GOAL>∀ (a : ℂ), (RCLike.complexLinearIsometryEquiv h).symm a = (RCLike.complexRingEquiv h).invFun a
<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<GOAL>∀ (a : ℂ), (RCLike.complexLinearIsometryEquiv h).invFun a = (RCLike.complexRingEquiv h).invFun a
<VAR>z : ℂ<VAR>hz : 0 ≤ z<GOAL>z = ↑‖z‖
<VAR>x : ℂ<GOAL>RCLike.re x = x.re
<VAR>x : ℂ<GOAL>RCLike.im x = x.im
<VAR>x : ℂ<GOAL>RCLike.normSq x = Complex.normSq x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>x : 𝕜<GOAL>HasSum (fun x => (starRingEnd 𝕜) (f x)) x ↔ HasSum f ((starRingEnd 𝕜) x)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>x : 𝕜<GOAL>HasSum (fun x => (starRingEnd 𝕜) (f x)) ((starRingEnd 𝕜) x) ↔ HasSum f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<GOAL>(Summable fun x => (starRingEnd 𝕜) (f x)) ↔ Summable f
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<GOAL>(starRingEnd 𝕜) (∑' (a : α), f a) = ∑' (a : α), (starRingEnd 𝕜) (f a)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → ℝ<VAR>x : ℝ<GOAL>HasSum (fun x => ↑(f x)) ↑x ↔ HasSum f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → ℝ<GOAL>(Summable fun x => ↑(f x)) ↔ Summable f
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → ℝ<GOAL>↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>x : 𝕜<VAR>h : HasSum f x<GOAL>HasSum (fun x => RCLike.re (f x)) (RCLike.re x)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>x : 𝕜<VAR>h : HasSum f x<GOAL>HasSum (fun x => RCLike.im (f x)) (RCLike.im x)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>h : Summable f<GOAL>RCLike.re (∑' (a : α), f a) = ∑' (a : α), RCLike.re (f a)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>h : Summable f<GOAL>RCLike.im (∑' (a : α), f a) = ∑' (a : α), RCLike.im (f a)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>c : 𝕜<GOAL>HasSum f c ↔ HasSum (fun x => RCLike.re (f x)) (RCLike.re c) ∧ HasSum (fun x => RCLike.im (f x)) (RCLike.im c)
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>x : ℂ<GOAL>HasSum (fun x => (starRingEnd ℂ) (f x)) x ↔ HasSum f ((starRingEnd ℂ) x)
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>x : ℂ<GOAL>HasSum (fun x => (starRingEnd ℂ) (f x)) ((starRingEnd ℂ) x) ↔ HasSum f x
<VAR>α : Type u_1<VAR>f : α → ℂ<GOAL>(Summable fun x => (starRingEnd ℂ) (f x)) ↔ Summable f
<VAR>α : Type u_1<VAR>f : α → ℂ<GOAL>(starRingEnd ℂ) (∑' (a : α), f a) = ∑' (a : α), (starRingEnd ℂ) (f a)
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>x : ℝ<GOAL>HasSum (fun x => ↑(f x)) ↑x ↔ HasSum f x
<VAR>α : Type u_1<VAR>f : α → ℝ<GOAL>(Summable fun x => ↑(f x)) ↔ Summable f
<VAR>α : Type u_1<VAR>f : α → ℝ<GOAL>↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>x : ℂ<VAR>h : HasSum f x<GOAL>HasSum (fun x => (f x).re) x.re
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>x : ℂ<VAR>h : HasSum f x<GOAL>HasSum (fun x => (f x).im) x.im
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>h : Summable f<GOAL>(∑' (a : α), f a).re = ∑' (a : α), (f a).re
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>h : Summable f<GOAL>(∑' (a : α), f a).im = ∑' (a : α), (f a).im
<VAR>α : Type u_1<VAR>f : α → ℂ<VAR>c : ℂ<GOAL>HasSum f c ↔ HasSum (fun x => (f x).re) c.re ∧ HasSum (fun x => (f x).im) c.im
<VAR>z : ℂ<GOAL>z ∈ Complex.slitPlane ↔ 0 < z.re ∨ z.im ≠ 0
<GOAL>Complex.slitPlane = {z | 0 < z.re} ∪ {z | z.im ≠ 0}
<VAR>x : ℝ<GOAL>↑x ∈ Complex.slitPlane ↔ 0 < x
<VAR>x : ℝ<GOAL>-↑x ∈ Complex.slitPlane ↔ x < 0
<VAR>n : ℕ<GOAL>↑n ∈ Complex.slitPlane ↔ n ≠ 0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ∈ Complex.slitPlane
<VAR>z : ℂ<GOAL>z ∈ Complex.slitPlane ↔ ¬z ≤ 0
<GOAL>(Set.Iic 0)ᶜ = Complex.slitPlane
<VAR>z : ℂ<VAR>hz : z ∈ Complex.slitPlane<GOAL>z ≠ 0
<GOAL>Metric.ball 1 1 ⊆ Complex.slitPlane
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>1 + z ∈ Complex.slitPlane
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>self : HasFDerivAtFilter f f' x L<GOAL>(fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<GOAL>HasFDerivAtFilter f f' x L ↔ (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x
<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>fderivWithin 𝕜 f s x = if 𝓝[s \ {x}] x = ⊥ then 0 else if h : ∃ f', HasFDerivWithinAt f f' s x then Classical.choose h else 0
<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>fderiv 𝕜 f x = if h : ∃ f', HasFDerivAt f f' x then Classical.choose h else 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>fderivWithin 𝕜 f s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : x ∉ closure s<GOAL>fderivWithin 𝕜 f s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>fderivWithin 𝕜 f s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>fderiv 𝕜 f x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Filter.Tendsto (fun n => ‖c n‖) l Filter.atTop<VAR>cdlim : Filter.Tendsto (fun n => c n • d n) l (𝓝 v)<GOAL>Filter.Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' f₁' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt f f₁' s x<GOAL>Set.EqOn (⇑f') (⇑f₁') (tangentConeAt 𝕜 s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' f₁' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>H : UniqueDiffWithinAt 𝕜 s x<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt f f₁' s x<GOAL>f' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' f₁' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>H : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>h : HasFDerivWithinAt f f' s x<VAR>h₁ : HasFDerivWithinAt f f₁' s x<GOAL>f' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<GOAL>HasFDerivAtFilter f f' x L ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<GOAL>HasFDerivWithinAt f f' s x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[s] x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<GOAL>HasFDerivAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<GOAL>HasFDerivAt f f' x ↔ (fun h => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖f'‖ ≤ ↑C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖f'‖ ≤ ↑C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L₁ L₂ : Filter E<VAR>h : HasFDerivAtFilter f f' x L₂<VAR>hst : L₁ ≤ L₂<GOAL>HasFDerivAtFilter f f' x L₁
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : HasFDerivWithinAt f f' t x<VAR>hst : t ∈ 𝓝[s] x<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : HasFDerivWithinAt f f' t x<VAR>hst : s ⊆ t<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>h : HasFDerivAt f f' x<VAR>hL : L ≤ 𝓝 x<GOAL>HasFDerivAtFilter f f' x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivAt f f' x<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<GOAL>HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<GOAL>HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : IsOpen s<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>y : E<GOAL>HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>g : E → F<VAR>g' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt g g' s x<GOAL>HasFDerivWithinAt g g' (insert x s) x