ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>inst✝ : NormedSpace ℂ E<VAR>hf : TorusIntegrable f c R<GOAL>∀ᵐ (a : Fin n → ℝ) ∂volume.restrict (Icc 0 fun x => 2 * π), ‖(∏ i : Fin n, ↑(R i) * cexp (↑(a i) * I) * I) • f (torusMap c R a)‖ ≤ (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>x.leadingCoeff = 0 ↔ x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>x.leadingCoeff = 0 → x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>x ≠ 0 → x.leadingCoeff ≠ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed (range down)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>s : Set β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>v : β → α<GOAL>((blimsup (s.piecewise u v) f fun x => x ∈ s) ⊔ blimsup (s.piecewise u v) f fun x => x ∉ s) = (blimsup u f fun x => x ∈ s) ⊔ blimsup v f fun x => x ∉ s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ (variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Equation 0 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>-(y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)) = 0 ↔ 1 ^ 6 * (W.a₆ + { u := 1, r := x, s := 0, t := y }.r * W.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W.a₂ + { u := 1, r := x, s := 0, t := y }.r ^ 3 - { u := 1, r := x, s := 0, t := y }.t * W.a₃ - { u := 1, r := x, s := 0, t := y }.t ^ 2 - { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W.a₁) = 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>∅ ∉ hC.diffFinset₀ hs hI
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<GOAL>¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<VAR>h✝ : Subsingleton R<GOAL>¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<VAR>h✝ : Nontrivial R<GOAL>¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<VAR>h✝ : Nontrivial R<GOAL>(¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hm : p.Monic<VAR>hnd : p.natDegree = 2<VAR>h✝ : Nontrivial R<GOAL>p ≠ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l l' : List α<VAR>h : l' ∈ sublistsLen (n + 1) (a :: l)<GOAL>l'.length = n + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l l' : List α<VAR>h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1 ∈ sublistsLen n l, a :: a_1 = l'<GOAL>l'.length = n + 1
<VAR>α : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : StarRing α<VAR>z : ↥(NonUnitalStarSubsemiring.center α)<VAR>a : α<GOAL>↑(star (centerToCentroidCenter z)) a = ↑(centerToCentroidCenter (star z)) a
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<VAR>hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<VAR>hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0<VAR>ν : Measure α := μ.restrict {a | M < f a}<VAR>this : SigmaFinite ν<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<VAR>hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0<VAR>ν : Measure α := μ.restrict {a | M < f a}<VAR>this : SigmaFinite ν<VAR>A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂ν<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<VAR>hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0<VAR>ν : Measure α := μ.restrict {a | M < f a}<VAR>this : SigmaFinite ν<VAR>A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂ν<VAR>B : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, ν {a | t ≤ f a} * ENNReal.ofReal (g t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>f_nonneg : ∀ (ω : α), 0 ≤ f ω<VAR>H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0<VAR>H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤<VAR>M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}<VAR>M_nonneg : 0 ≤ M<VAR>hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0<VAR>ν : Measure α := μ.restrict {a | M < f a}<VAR>this : SigmaFinite ν<VAR>A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂ν<VAR>B : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, ν {a | t ≤ f a} * ENNReal.ofReal (g t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂ν = ∫⁻ (t : ℝ) in Ioi 0, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.ΨSq (2 * (↑m + 3)) = (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>((cyclotomic p ℤ).comp (X + 1)).IsEisensteinAt (Submodule.span ℤ {↑p})
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>((cyclotomic p ℤ).comp (X + 1)).Monic
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>i : ℕ<VAR>hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree<GOAL>((cyclotomic p ℤ).comp (X + 1)).coeff i ∈ Submodule.span ℤ {↑p}
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>((cyclotomic p ℤ).comp (X + 1)).coeff 0 ∉ Submodule.span ℤ {↑p} ^ 2
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : Fin n → ℂ<VAR>R θ : Fin n → ℝ<GOAL>torusMap c R θ = c ↔ R = 0
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ oddKernel a =O[atTop] fun x => rexp (-p * x)
<VAR>b : ℝ<GOAL>∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x => rexp (-p * x)
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x => rexp (-p * x)
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)<GOAL>∀ᶠ (x : ℝ) in atTop, ‖oddKernel (↑b) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) x
<VAR>b p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖oddKernel (↑b) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) t
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ<VAR>this : ↑z1 = ↑z2 ↔ z1 = z2<GOAL>↑z1 = ↑z2 ↔ ↑z1 = ↑z2
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ<GOAL>↑z1 = ↑z2 ↔ z1 = z2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x y : K<GOAL>spanSingleton R₁⁰ x / spanSingleton R₁⁰ y = spanSingleton R₁⁰ (x / y)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>h : ∀ (t : ℝ), IsIntegralCurveAt γ v t<VAR>t : ℝ<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>h✝ : ∀ (t : ℝ), IsIntegralCurveAt γ v t<VAR>t : ℝ<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t<VAR>h : IsIntegralCurveOn γ v s<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hIP : comap (algebraMap R S) I ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>P' : Ideal S<VAR>hP : P' ≥ I<VAR>hP' : P'.IsPrime<VAR>hP'' : comap (algebraMap R S) P' ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>I : Ideal S<VAR>hIP : comap (algebraMap R S) I ≤ P<VAR>P' : Ideal S<VAR>hP : P' ≥ I<VAR>hP' : P'.IsPrime<VAR>hP'' : comap (algebraMap R S) P' ≤ P<VAR>Q : Ideal S<VAR>hQ : Q ≥ P'<VAR>hQ' : Q.IsPrime<VAR>hQ'' : comap (algebraMap R S) Q = P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>n : ℕ<GOAL>(map (natEmbedding α) (range n)).card = n
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>star a * a = ↑(normSq a)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>h : a ∈ s<VAR>hba : b * a ∈ s<GOAL>b ∈ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>ι : Type u_7<VAR>m : ι → Measure α<VAR>μ : Measure β<VAR>inst✝ : SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>((sum m).prod μ) s = (sum fun i => (m i).prod μ) s
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>(∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>∑ a_1 : Perm.ModSumCongr ιa ιb, (domCoprod.summand a b a_1) v = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivAt I' I'' g (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f')
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivWithinAt I' I'' g univ (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f')
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z p₁ p₂ p : P<GOAL>p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i k‖ = a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i k‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>hj : j ∈ Ico 2 (n + 1)<GOAL>a ^ j * ‖p.rightInv i j‖ = a ^ j * ‖(↑i.symm).compContinuousMultilinearMap (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c)‖