ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²³ : Semiring R₁<VAR>inst✝²² : Semiring R₂<VAR>inst✝²¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M₁<VAR>inst✝¹⁹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁸ : TopologicalSpace M'₁<VAR>inst✝¹⁷ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace M₂<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁴ : TopologicalSpace M₃<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹² : TopologicalSpace M₄<VAR>inst✝¹¹ : AddCommMonoid M₄<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>inst✝⁹ : Module R₁ M'₁<VAR>inst✝⁸ : Module R₂ M₂<VAR>inst✝⁷ : Module R₃ M₃<VAR>inst✝⁶ : RingHomSurjective σ₁₂<VAR>inst✝⁵ : TopologicalSpace R₁<VAR>inst✝⁴ : TopologicalSpace R₂<VAR>inst✝³ : ContinuousSMul R₁ M₁<VAR>inst✝² : ContinuousAdd M₁<VAR>inst✝¹ : ContinuousSMul R₂ M₂<VAR>inst✝ : ContinuousAdd M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf' : DenseRange ⇑f<VAR>s : Submodule R₁ M₁<VAR>hs : Dense ↑s<GOAL>Dense ↑(Submodule.map (↑f) s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>(⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝¹ b✝¹ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b / min a b = mabs (b / a)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set ι<VAR>this : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)<GOAL>AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set ι<VAR>this✝ : aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)<VAR>this : ∀ (p : MvPolynomial (↑s) R), (rename Subtype.val) p = 0 ↔ p = 0<GOAL>AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>h's : s ⊆ u<VAR>h't : t ⊆ u<VAR>h : μ u < μ s + μ t<GOAL>(s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>h's : s ⊆ u<VAR>h't : t ⊆ u<VAR>h : μ u < μ t + μ s<GOAL>(s ∩ t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>h's : s ⊆ u<VAR>h't : t ⊆ u<VAR>h : μ u < μ t + μ s<GOAL>(t ∩ s).Nonempty
<VAR>a b : ℤ<GOAL>(EuclideanDomain.gcd a b).natAbs = a.gcd b
<VAR>a b : ℤ<GOAL>↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)
<VAR>a b : ℤ<GOAL>↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Free R M₁<VAR>inst✝ : Finite R M<GOAL>finrank R M = Fintype.card (ChooseBasisIndex R M)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>ns : List ℕ<VAR>i : ℕ<VAR>hi : i < (l.splitWrtCompositionAux ns).length<GOAL>(l.splitWrtCompositionAux ns).get ⟨i, hi⟩ = drop (take i ns).sum (take (take (i + 1) ns).sum l)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>ι : Type u_2<VAR>xs : ι → α<VAR>xs_dense : DenseRange xs<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ i, ball (xs i) U = univ
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>ι : Type u_2<VAR>xs : ι → α<VAR>xs_dense : DenseRange xs<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ x ∈ range xs, ball x U = univ
<VAR>G : Type u<VAR>inst✝¹ : CancelCommMonoid G<VAR>inst✝ : Fintype G<GOAL>exponent G = (Finset.image orderOf Finset.univ).max' ⋯
<VAR>G : Type u<VAR>inst✝¹ : CancelCommMonoid G<VAR>inst✝ : Fintype G<GOAL>exponent G = iSup orderOf
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[m + n.succ] = f^[m] ∘ f^[n.succ]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<GOAL>(f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A * B).card * (B / C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C⁻¹).card * B.card ≤ (A * B).card * (B * C⁻¹).card
<VAR>R : Type u_1<VAR>S : Type ?u.122514<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.122979<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.124119<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝ : Module.Finite R M<GOAL>Subsingleton (k ⊗[R] M) ↔ Subsingleton M
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>inst✝ : IsDomain R₁<VAR>M : Matrix ι ι R₁<GOAL>((toLinearMap₂' R₁) M).SeparatingLeft ↔ M.det ≠ 0
<VAR>a✝ b n✝ n a : ℕ<GOAL>(n.ceilRoot a).factorization = a.factorization ⌈/⌉ n
<VAR>a✝ b n✝ n a : ℕ<GOAL>(if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x x_1 => x ^ x_1).factorization = a.factorization ⌈/⌉ n
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<GOAL>((a.factorization ⌈/⌉ n).prod fun x x_1 => x ^ x_1).factorization = a.factorization ⌈/⌉ n
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<VAR>p : ℕ<VAR>hp : p ∈ (a.factorization ⌈/⌉ n).support<GOAL>Prime p
<VAR>a✝ b n✝ n a : ℕ<VAR>h : ¬(n = 0 ∨ a = 0)<VAR>p : ℕ<VAR>hp : p ∈ (a.factorization ⌈/⌉ n).support<VAR>this : Prime p ∧ p ∣ a ∧ ¬a = 0<GOAL>Prime p
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : l ≠ []<VAR>i j : ℕ<VAR>h : l.rotate i = l.rotate j<GOAL>i % l.length = j % l.length
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : l ≠ []<VAR>i j : ℕ<VAR>h : l.rotate (i % l.length) = l.rotate (j % l.length)<GOAL>i % l.length = j % l.length
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ ∫ (a : D), 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂) ∂μ
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>0 ≤ᶠ[ae μ] fun a => ‖a‖ ^ k * ‖f a‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>Integrable (fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)) μ
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>(fun a => ‖a‖ ^ k * ‖f a‖) ≤ᶠ[ae μ] fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<VAR>v : D<GOAL>‖v‖ ^ k * ‖f v‖ ≤ 2 ^ μ.integrablePower * (1 + ‖v‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : eval x (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, X ^ i)<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i<VAR>h : 0 < ∑ i ∈ range n, x ^ i<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i<VAR>h : 0 = ∑ i ∈ range n, x ^ i<GOAL>0 < eval x (cyclotomic n R)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>x : R<VAR>n : ℕ<VAR>ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)<VAR>hn : 2 < n<VAR>hn' : 0 < n<VAR>hn'' : 1 < n<VAR>this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i<VAR>h : ∑ i ∈ range n, x ^ i < 0<GOAL>0 < eval x (cyclotomic n R)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<GOAL>Group.IsNilpotent ↥(frattini G)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<VAR>q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal<GOAL>Group.IsNilpotent ↥(frattini G)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>p_prime : Fact (Nat.Prime p)<VAR>P : Sylow p ↥(frattini G)<GOAL>(↑P).Normal
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>p_prime : Fact (Nat.Prime p)<VAR>P : Sylow p ↥(frattini G)<VAR>frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤<GOAL>(↑P).Normal
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>p_prime : Fact (Nat.Prime p)<VAR>P : Sylow p ↥(frattini G)<VAR>frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤<VAR>normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤<GOAL>(↑P).Normal
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>p_prime : Fact (Nat.Prime p)<VAR>P : Sylow p ↥(frattini G)<VAR>frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤<VAR>normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤<VAR>P_normal_in_G : (map (frattini G).subtype ↑P).Normal<GOAL>(↑P).Normal
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x✝ y✝ z x y : 𝕜<GOAL>[x-[𝕜]y] = Icc (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x✝ y✝ z x y : 𝕜<VAR>h : x ≤ y<GOAL>[x-[𝕜]y] = Icc (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x✝ y✝ z x y : 𝕜<VAR>h : y ≤ x<GOAL>[x-[𝕜]y] = Icc (min x y) (max x y)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s - t + s ∩ t = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s - t + t ∩ s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t✝ u : Multiset α<VAR>a b : α<VAR>t : Multiset α<GOAL>∀ (s : Multiset α), s - t + t ∩ s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝¹ u : Multiset α<VAR>a✝ b : α<VAR>t✝ : Multiset α<VAR>a : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), s - t + t ∩ s = s<VAR>s : Multiset α<GOAL>s - a ::ₘ t + (a ::ₘ t) ∩ s = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → G<GOAL>‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → G<VAR>le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖<GOAL>‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹³ : CommRing R₁<VAR>inst✝¹² : AddCommGroup M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : CommRing R₃<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>inst✝¹ : Fintype n<VAR>b : Basis n R₃ M₃<VAR>J J₃ A A' : Matrix n n R₃<VAR>inst✝ : DecidableEq n<GOAL>A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsHomLift f φ<GOAL>p.obj b = S
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsHomLift (p.map φ) φ<GOAL>p.obj b✝ = p.obj b✝
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>logb b x ≤ y ↔ b ^ y ≤ x
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i✝ : ι<VAR>g✝ : G i✝<VAR>w : NormalWord d<VAR>hmw : w.fstIdx ≠ some i✝<VAR>hgr : g✝ ∉ (φ i✝).range<VAR>n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv (g✝ * (φ i✝) w.head)<VAR>w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯<VAR>i : ι<VAR>g : G i<VAR>hg : ⟨i, g⟩ ∈ w'.toList<GOAL>g ∈ d.set i
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i✝ : ι<VAR>g✝ : G i✝<VAR>w : NormalWord d<VAR>hmw : w.fstIdx ≠ some i✝<VAR>hgr : g✝ ∉ (φ i✝).range<VAR>n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv (g✝ * (φ i✝) w.head)<VAR>w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯<VAR>i : ι<VAR>g : G i<VAR>hg : i = i✝ ∧ HEq g ↑n.2 ∨ ⟨i, g⟩ ∈ w.toList<GOAL>g ∈ d.set i
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>constantCoeff ((monomial d) r) = if d = 0 then r else 0
<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>inst✝⁶ : SmoothManifoldWithCorners I 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>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑I.symm) (range ↑I)
<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>inst✝⁶ : SmoothManifoldWithCorners I 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>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousOn (↑I.symm) (range ↑I) ∧ ∀ (x : E) (y : H), ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm) ((extChartAt 𝓘(𝕜, E) x).target ∩ ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))