ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' s)
<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 P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x => x -ᵥ p) '' s)
<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 P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x => x -ᵥ p) '' s)
<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 P<VAR>p : P<VAR>hp : p ∈ s<GOAL>(fun x => x -ᵥ p) '' s ⊆ s -ᵥ s
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<GOAL>∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<GOAL>∫ (a : X), (NNReal.toReal ∘ ⇑f.nnrealPart) a ∂μ - ∫ (a : X), (NNReal.toReal ∘ ⇑(-f).nnrealPart) a ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<GOAL>χ₀ n (g * h) = χ₀ n g * χ₀ n h
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<VAR>ζ : ↥(rootsOfUnity n L)<GOAL>(g * h) ↑↑ζ = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<VAR>ζ : ↥(rootsOfUnity n L)<GOAL>g (h ↑↑ζ) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<VAR>ζ : ↥(rootsOfUnity n L)<GOAL>↑↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑(↑ζ ^ (χ₀ n h * χ₀ n g).val)
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g h : L ≃+* L<VAR>ζ : ↥(rootsOfUnity n L)<GOAL>ζ ^ ((χ₀ n h).val * (χ₀ n g).val) = ζ ^ (χ₀ n h * χ₀ n g).val
<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>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>p2 -ᵥ p ∈ s.direction ↔ p2 ∈ s
<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>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>p2 : P<GOAL>(∃ p2_1 ∈ s, p2 -ᵥ p = p2_1 -ᵥ p) ↔ p2 ∈ 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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>c : E<GOAL>a * c ∈ ball (b * c) r ↔ a ∈ ball b r
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>h : p ≤ q<GOAL>ENNReal.ofReal p ≤ ENNReal.ofReal q
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Group G✝<VAR>A✝ : Rep k✝ G✝<VAR>k G A : Type u<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module k A<VAR>inst✝¹ : DistribMulAction G A<VAR>inst✝ : SMulCommClass G k A<VAR>f : ↥(twoCoboundaries (Rep.ofDistribMulAction k G A))<GOAL>IsTwoCoboundary ↑↑f
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Group G✝<VAR>A✝ : Rep k✝ G✝<VAR>k G A : Type u<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module k A<VAR>inst✝¹ : DistribMulAction G A<VAR>inst✝ : SMulCommClass G k A<VAR>f : ↥(twoCoboundaries (Rep.ofDistribMulAction k G A))<VAR>x : G → CoeSort.coe (Rep.ofDistribMulAction k G A)<VAR>hx : (dOne (Rep.ofDistribMulAction k G A)) x = (twoCocycles (Rep.ofDistribMulAction k G A)).subtype ↑f<GOAL>IsTwoCoboundary ↑↑f
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f : P.B a ⟹ α ::: P.W α<GOAL>P.wDest' (P.wMk' ⟨a, f⟩) = ⟨a, f⟩
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<GOAL>M.charmatrix.det.coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<GOAL>∑ b : Equiv.Perm n, (Equiv.Perm.sign b • ∏ i : n, M.charmatrix (b i) i).coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<GOAL>∀ c ∈ univ, (Equiv.Perm.sign c • ∏ i : n, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<VAR>c : Equiv.Perm n<GOAL>(Equiv.Perm.sign c • ∏ i : n, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<VAR>c : Equiv.Perm n<GOAL>(∏ i : n, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<VAR>c : Equiv.Perm n<VAR>this : ∑ x : n, 1 = Fintype.card n<GOAL>(∏ i : n, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<VAR>c : Equiv.Perm n<VAR>this : ∑ x : n, 1 = Fintype.card n<GOAL>(∏ i : n, M.charmatrix (c i) i).coeff k ∈ I ^ (∑ x : n, 1 - k)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<VAR>c : Equiv.Perm n<VAR>this : ∑ x : n, 1 = Fintype.card n<GOAL>∀ i ∈ univ, ∀ (k : ℕ), (M.charmatrix (c i) i).coeff k ∈ I ^ (1 - k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<VAR>l : f.LimZero<GOAL>g.LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<VAR>l : g.LimZero<GOAL>f.LimZero
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α✝<VAR>inst✝² : Nonempty α✝<VAR>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>x : α<GOAL>x ∈ (uniformOfFintype α).support ↔ x ∈ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>s : Finset α<GOAL>s.toList = [a] ↔ s = {a}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>MonovaryOn f g s ↔ (∀ x ∈ s, ∀ x_2 ∈ s, f x < f x_2 → g x ≤ g x_2) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, g x < g x_2 → f x ≤ f x_2
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>C : A → Prop<VAR>r : A<VAR>hr : r ∈ M * N<VAR>hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)<VAR>ha : ∀ (x y : A), C x → C y → C (x + y)<GOAL>C r
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>C : A → Prop<VAR>r : A<VAR>hr : r ∈ M.toAddSubmonoid * N.toAddSubmonoid<VAR>hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)<VAR>ha : ∀ (x y : A), C x → C y → C (x + y)<GOAL>C r
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>card σ.cycleType = 1 ↔ σ.IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>(∃ a, σ.cycleType = {a}) ↔ σ.IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>(∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<GOAL>ContinuousAt (⇑p) 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>p.closedBall 0 ε ∈ 𝓝 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>hp : p.closedBall 0 r ∈ 𝓝 0<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>k : 𝕜<VAR>hk₀ : 0 < ‖k‖<VAR>hk : ‖k‖ * r < ε<GOAL>p.closedBall 0 ε ∈ 𝓝 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>r ε : ℝ<VAR>hε : ε > 0<VAR>k : 𝕜<VAR>hp : p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0<VAR>hk₀ : 0 < ‖k‖<VAR>hk : ‖k‖ * r < ε<GOAL>p.closedBall 0 ε ∈ 𝓝 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<GOAL>padicNorm p (q * r) = padicNorm p q * padicNorm p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>this : ↑p ≠ 0<GOAL>padicNorm p (q * r) = padicNorm p q * padicNorm p r
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<GOAL>(-a).valMinAbs = -a.valMinAbs
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<VAR>h : n = 0<GOAL>(-a).valMinAbs = -a.valMinAbs
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<VAR>h : NeZero n<GOAL>(-a).valMinAbs = -a.valMinAbs
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<VAR>h : NeZero n<GOAL>-a = ↑(-a.valMinAbs)
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<VAR>h : NeZero n<GOAL>-↑n < -a.valMinAbs * 2
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<VAR>h : NeZero n<GOAL>-a.valMinAbs * 2 ≤ ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : R<GOAL>{r} - σ a = σ (↑ₐ r - a)
<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>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>J : FractionalIdeal A⁰ K<VAR>hJ : J ≠ 0<VAR>I I' : FractionalIdeal A⁰ K<GOAL>J * I ≤ J * I' ↔ I ≤ I'
<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>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>J : FractionalIdeal A⁰ K<VAR>hJ : J ≠ 0<VAR>I I' : FractionalIdeal A⁰ K<GOAL>J * I ≤ J * I' ↔ I * J ≤ I' * J
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>x t : G<VAR>s : Set G<VAR>hx : x ∈ s<GOAL>‖(L (f (x - t))) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>x t : G<VAR>s : Set G<VAR>hx : x ∈ s<GOAL>(-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t = (-tsupport f + s).indicator (fun t => ‖L.flip‖ * ‖g t‖ * ⨆ i, ‖f i‖) t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝¹ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Nontrivial R<GOAL>(if e ∈ G.incidenceSet a then 1 e else 0) = 1 ↔ e ∈ G.incidenceSet a
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝¹ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Nontrivial R<GOAL>(if e ∈ G.incidenceSet a then 1 else 0) = 1 ↔ e ∈ G.incidenceSet a
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<GOAL>p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>m₃ : M₃<GOAL>m₃ ∈ LinearMap.range (↑g ∘ₗ TensorProduct.mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x)) → m₃ ∈ 𝕎(M₃, χ₁ + χ₂, x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>m₃ : M₃<GOAL>∀ (x_1 : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)), g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) x_1) = m₃ → ∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) m₃ = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<GOAL>∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t)) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<GOAL>∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) 0)) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<GOAL>∀ (x_1 : ↥𝕎(M₁, χ₁, x)) (y : ↥𝕎(M₂, χ₂, x)), ∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (x_1 ⊗ₜ[R] y))) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<GOAL>∀ (x_1 y : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)), (∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) x_1)) = 0) → (∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) y)) = 0) → ∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (x_1 + y))) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)<VAR>m₂ : M₂<VAR>hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<GOAL>∃ k, (F ^ k) (↑g (m₁ ⊗ₜ[R] m₂)) = 0