ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>r : S<VAR>hr : ¬r = 0<VAR>this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<GOAL>↑ℤ (Submodule.subtype (span {r})) ∘ₗ (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap = (Algebra.lmul ℤ S) r
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>r : S<VAR>hr : ¬r = 0<VAR>this : Fintype (S ⧸ span {r}) := (span {r}).fintypeQuotientOfFreeOfNeBot ⋯<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>i : Module.Free.ChooseBasisIndex ℤ S<GOAL>(↑ℤ (Submodule.subtype (span {r})) ∘ₗ (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap) (b i) = ((Algebra.lmul ℤ S) r) (b i)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>r : ℝ<GOAL>edist x y < ENNReal.ofReal r ↔ dist x y < r
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ × α → β<GOAL>∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>r : Finset (γ × α)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1<VAR>f : γ × α → β<GOAL>∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.fst, x.snd)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a ≤ b<GOAL>⌊a⌋₊ ≤ ⌊b⌋₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a ≤ b<VAR>ha : a ≤ 0<GOAL>⌊a⌋₊ ≤ ⌊b⌋₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a ≤ b<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ ≤ ⌊b⌋₊
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : DivisionRing R<VAR>p q : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<GOAL>(map f p).leadingCoeff = f p.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>i : ι := Classical.arbitrary ι<GOAL>p.basisSets.Nonempty
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>i : ι := Classical.arbitrary ι<GOAL>(p i).ball 0 1 ∈ p.basisSets
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : C ⥤ D<VAR>R₁ R₂ R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : R₁ ⟶ R₂<VAR>β : R₂ ⟶ R₃<GOAL>(conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : C ⥤ D<VAR>R₁ R₂ R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : R₁ ⟶ R₂<VAR>β : R₂ ⟶ R₃<GOAL>(conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫ (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) = α ≫ β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>sSup s = sSup univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>¬BddAbove univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>hs : BddAbove univ<GOAL>BddAbove s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsCompact (⇑h ⁻¹' s) ↔ IsCompact s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsCompact (⇑h.symm '' s) ↔ IsCompact s
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinitesimal<VAR>hp : 0 < x<VAR>hy : y.InfiniteNeg<GOAL>(x * y).InfiniteNeg
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinitesimal<VAR>hp : 0 < x<VAR>hy : y.InfiniteNeg<GOAL>(y * x).InfiniteNeg
<VAR>α : Type u_1<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>card α = card αˣ + 1
<VAR>α : Type u_1<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>card { a // a ≠ 0 } + 1 = card α
<VAR>α : Type u_1<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>this : card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) = card α<GOAL>card { a // a ≠ 0 } + 1 = card α
<VAR>a x z : ℂ<VAR>θ : ℝ<GOAL>(cexp (↑θ * I)).arg = toIocMod ⋯ (-π) θ
<VAR>a x z : ℂ<VAR>θ : ℝ<GOAL>cexp (↑θ * I) = cos ↑(toIocMod ⋯ (-π) θ) + sin ↑(toIocMod ⋯ (-π) θ) * I
<VAR>a x z : ℂ<VAR>θ : ℝ<GOAL>toIocMod ⋯ (-π) θ ∈ Ioc (-π) π
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ<GOAL>eigenspace (T.restrict ⋯) μ = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ<GOAL>Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ<VAR>H₂ : eigenspace T μ ⟂ p<GOAL>Disjoint (eigenspace T μ) (⨆ μ, eigenspace T μ)ᗮ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>x : V<VAR>hx : x ∈ ↑(affineSpan k s)<GOAL>x ∈ Submodule.span k s
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} 𝒳<VAR>inst✝² : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b c : 𝒳<VAR>R : 𝒮<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsHomLift (𝟙 R) φ<VAR>S T : 𝒮<VAR>f : S ⟶ T<VAR>ψ : b ⟶ c<VAR>inst✝ : p.IsHomLift f ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} 𝒳<VAR>inst✝² : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b c : 𝒳<VAR>R : 𝒮<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsHomLift (𝟙 R) φ<VAR>T : 𝒮<VAR>ψ : b ⟶ c<VAR>f : R ⟶ T<VAR>inst✝ : p.IsHomLift f ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>v : Fin 1 → E<GOAL>(id 𝕜 E 1) v = v ⟨0, ⋯⟩
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>x : R<VAR>w : p ≠ 0<GOAL>x ∈ p.roots ↔ (aeval x) p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>x : R<VAR>w : p ≠ 0<GOAL>eval x p = 0 ↔ eval x (map (algebraMap R R) p) = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<VAR>hi : ¬c.Rel (c.prev i) i<GOAL>f i (c.prev i) ≫ D.d (c.prev i) i = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>seminormFromConst' hf1 hc hpm x ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>∀ (b : ℕ), 1 ≤ b → seminormFromConst_seq c f x b ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>n : ℕ<VAR>hn : 1 ≤ n<GOAL>seminormFromConst_seq c f x n ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>n : ℕ<VAR>hn : 1 ≤ n<GOAL>f x * f (c ^ n) / f c ^ n ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s s' t : Set α<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>t.ite s s' ∩ closure t = s ∩ closure t
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<GOAL>0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>b : n<VAR>M : Matrix n n α<GOAL>(stdBasisMatrix i j c * M) i b = c * M j b
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>μ ≪ μ.inv
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>x✝ : MeasurableSet s<GOAL>μ.inv s = 0 → μ s = 0
<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>p.1 ≠ 0 ∧ p.2 ≠ 0
<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<VAR>hp₁ : p.1 * p.2 = n<VAR>hp₂ : n ≠ 0<GOAL>p.1 ≠ 0 ∧ p.2 ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>hc1 : MellinConvergent (fun x => P.f x - P.f₀) s<GOAL>mellin (fun x => P.f x - P.f₀) s = P.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>hc1 : MellinConvergent (fun x => P.f x - P.f₀) s<VAR>hc2 : HasMellin P.f_modif s (P.Λ₀ s)<GOAL>mellin (fun x => P.f x - P.f₀) s = P.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>hc1 : MellinConvergent (fun x => P.f x - P.f₀) s<VAR>hc2 : HasMellin P.f_modif s (P.Λ₀ s)<VAR>hc3 : mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀<GOAL>mellin (fun x => P.f x - P.f₀) s = P.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>hc1 : MellinConvergent (fun x => P.f x - P.f₀) s<VAR>hc2 : HasMellin P.f_modif s (P.Λ₀ s)<VAR>hc3 : mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀<VAR>this : mellin (fun t => P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun x => P.f x - P.f₀) s<GOAL>mellin (fun x => P.f x - P.f₀) s = P.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>hc1 : MellinConvergent (fun x => P.f x - P.f₀) s<VAR>hc2 : HasMellin P.f_modif s (P.Λ₀ s)<VAR>hc3 : mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀<VAR>this : mellin (fun x => P.f x - P.f₀) s = mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / (↑P.k - s)) • P.g₀<GOAL>mellin (fun x => P.f x - P.f₀) s = P.Λ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : R<VAR>hr : ‖r‖ < 1<GOAL>Summable fun n => ‖↑n ^ k * r ^ n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r : R<VAR>hr : ‖r‖ < 1<VAR>r' : ℝ<VAR>hrr' : ‖r‖ < r'<VAR>h : r' < 1<GOAL>Summable fun n => ‖↑n ^ k * r ^ n‖
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>V : Set X<GOAL>s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<VAR>r' : α → α → Prop<VAR>hr' : Reflexive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : ReflGen r x y<GOAL>r' x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝ n : ℕ<VAR>xs✝ : List α<VAR>a : α<VAR>xs : List α<VAR>z : Sym α 0<VAR>ha : a ∈ z<VAR>hz : z ∈ List.sym 0 xs<GOAL>a ∈ xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝ n : ℕ<VAR>xs✝ : List α<VAR>a : α<VAR>xs : List α<VAR>ha : a ∈ Sym.nil<VAR>hz : Sym.nil ∈ List.sym 0 xs<GOAL>a ∈ xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>a : α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>z : Sym α (n + 1)<VAR>ha : a ∈ z<VAR>hz : z ∈ List.sym (n + 1) (x :: xs)<GOAL>a ∈ x :: xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>a : α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>z : Sym α (n + 1)<VAR>ha : a ∈ z<VAR>hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs<GOAL>a ∈ x :: xs
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p✝ : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<VAR>hp : ¬p = 0<GOAL>(k • p).natDegree = p.natDegree
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p✝ : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<VAR>hp : ¬p = 0<GOAL>k • p ≠ 0
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p✝ : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<VAR>hp : k • p = 0<GOAL>p = 0
<VAR>R : Type u<VAR>S✝ : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>p✝ : R[X]<VAR>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<VAR>hp : k • p = k • 0<GOAL>p = 0
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α✝<VAR>inst✝¹ : OrderBot α✝<VAR>s✝ s₁ s₂ : Finset β✝<VAR>f✝ g : β✝ → α✝<VAR>a✝ : α✝<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(s.sup fun b => f b \ a) = s.sup f \ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v✝ v₁ v₂ : VectorMeasure α M✝<VAR>w✝ w₁ w₂ : VectorMeasure α N<VAR>M : Type u_6<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>u : Set α<VAR>hmu : MeasurableSet u<VAR>hu₁ : ∀ t ⊆ u, ↑v t = 0<VAR>hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0<VAR>s : Set α<VAR>hs : s ⊆ u<GOAL>↑(-v) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v✝ v₁ v₂ : VectorMeasure α M✝<VAR>w✝ w₁ w₂ : VectorMeasure α N<VAR>M : Type u_6<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>u : Set α<VAR>hmu : MeasurableSet u<VAR>hu₁ : ∀ t ⊆ u, ↑v t = 0<VAR>hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0<VAR>s : Set α<VAR>hs : s ⊆ u<GOAL>↑v s = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<GOAL>(sum fun g => ν.restrict (g • s)) = ν
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<VAR>this : Module.rank R (M ⧸ N) ≠ 0<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<VAR>this : ¬∀ (x : M), ∃ a, a ≠ 0 ∧ a • Submodule.Quotient.mk x = 0<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<VAR>this : ∃ x, ∀ (a : R), a ≠ 0 → a • Submodule.Quotient.mk x ≠ 0<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<VAR>this : ∃ x, ∀ (a : R), ¬a = 0 → a • x ∉ N<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>Tendsto (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) atTop (𝓝 (spectralRadius ℂ a))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>(fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) = fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>x✝ : ℕ<GOAL>ENNReal.ofReal (‖a ^ x✝‖ ^ (1 / ↑x✝)) = ↑‖a ^ x✝‖₊ ^ (1 / ↑x✝)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>x✝ : ℕ<GOAL>0 ≤ 1 / ↑x✝
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔ x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔ x ∈ ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(∃ a, (mixedEmbedding K).toIntAlgHom.toLinearMap ((algebraMap (𝓞 K) K) a) = x) ↔ ∃ x_1, ((mixedEmbedding K).comp (algebraMap (𝓞 K) K)) x_1 = x
<VAR>x y y₁ y₂ : PGame<VAR>hx : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<GOAL>∀ {x₁ x₂ : PGame}, x₁.Numeric → x₂.Numeric → x₁ < x₂ → P3 x₁ x₂ y₁ y₂
<VAR>x y y₁ y₂ : PGame<VAR>hx : x.Numeric<VAR>hy✝ : y.Numeric<VAR>hy₁ : y₁.Numeric<VAR>hy₂ : y₂.Numeric<VAR>hy : y₁ < y₂<GOAL>∀ (x : PGame × PGame), x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂