ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a : α<VAR>ha : a ∈ s<GOAL>(map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod ↔ (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a : α<VAR>ha : a ∈ A<GOAL>(map f (s + replicate (n - m) a)).prod = (map f (t + replicate (n - m) a)).prod ↔ (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a✝ : α<VAR>ha✝ : a✝ ∈ A<VAR>a : α<VAR>ha : a ∈ s + replicate (n - m) a✝<GOAL>a ∈ A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a✝ : α<VAR>ha✝ : a✝ ∈ A<VAR>a : α<VAR>ha : a ∈ t + replicate (n - m) a✝<GOAL>a ∈ A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a : α<VAR>ha : a ∈ A<GOAL>card (s + replicate (n - m) a) = n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a : α<VAR>ha : a ∈ A<GOAL>card (t + replicate (n - m) a) = n
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ 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>this : P.Λ₀ (↑P.k - s) = P.ε • P.symm.Λ₀ s<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ 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>this : P.Λ (↑P.k - s) + (1 / (↑P.k - s)) • P.f₀ + (P.ε / s) • P.g₀ = P.ε • (P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀)<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<GOAL>chaar K₀ ⊥ = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>chaar K₀ ⊥ = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>chaar K₀ ∈ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥<VAR>this : Continuous eval<GOAL>IsClosed (eval ⁻¹' {0})
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>((expSeries ℝ ℍ (2 * n + 1)) fun x => q) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<GOAL>(↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>n : ℕ<VAR>hq : re 0 = 0<GOAL>(↑(2 * n + 1)!)⁻¹ • 0 ^ (2 * n + 1) = ((-1) ^ n * ‖0‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖0‖) • 0
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<GOAL>(↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<VAR>hq2 : q ^ 2 = -↑(normSq q)<GOAL>(↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>hqn : ‖q‖ ≠ 0<GOAL>(↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>hqn : ‖q‖ ≠ 0<VAR>k : ℝ := ↑(2 * n + 1)!<GOAL>(↑(2 * n + 1)!)⁻¹ • q ^ (2 * n + 1) = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)! / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>hqn : ‖q‖ ≠ 0<VAR>k : ℝ := ↑(2 * n + 1)!<GOAL>k⁻¹ • ((-↑(normSq q)) ^ n * q) = k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>n : ℕ<VAR>hq0 : q ≠ 0<VAR>hq2 : q ^ 2 = -↑(normSq q)<VAR>hqn : ‖q‖ ≠ 0<VAR>k : ℝ := ↑(2 * n + 1)!<GOAL>k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_3<VAR>m : Type u_4<VAR>R : Type u_5<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>hA : A.IsSymm<VAR>hBC : Bᵀ = C<VAR>hD : D.IsSymm<VAR>hCB : Cᵀ = B<GOAL>(Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
<VAR>l m r : List Char<GOAL>{ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.next { byteIdx := utf8Len m } = { byteIdx := utf8Len m }
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝² : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>A : Type u<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Nontrivial A<VAR>a b : ℕ<VAR>h : a.Coprime b<GOAL>IsCoprime ↑a ↑b
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>a : (i : ι) → π i<GOAL>I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<GOAL>⋃ i, ⋃ (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, ∃ (hi : p i), x ≤ f i hi
<VAR>a y k : ℕ<VAR>hy0 : y ≠ 0<VAR>hk0 : k ≠ 0<VAR>hyk : y ^ k < a<VAR>hya : y < a<GOAL>↑a ≤ ↑a ^ 2 - (↑a - 1) ^ 2 - 1
<VAR>a y k : ℕ<VAR>hy0 : y ≠ 0<VAR>hk0 : k ≠ 0<VAR>hyk : y ^ k < a<VAR>hya : y < a<GOAL>1 < ↑a
<VAR>a y k : ℕ<VAR>hy0 : y ≠ 0<VAR>hk0 : k ≠ 0<VAR>hyk : y ^ k < a<VAR>hya : y < a<GOAL>1 < a
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x : K<GOAL>extension (↑K x) = v x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x : K<GOAL>Tendsto (⇑v) (Filter.comap (↑K) (𝓝 (↑K x))) (𝓝 (v x))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>hv : Valued K Γ₀<VAR>x : K<GOAL>Tendsto (⇑v) (𝓝 x) (𝓝 (v x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<VAR>ht_pos : 0 < t<GOAL>(μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist t u ≠ ⊤<GOAL>hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist u t ≠ ⊤<GOAL>hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist u t ≠ ⊤<VAR>I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s<GOAL>hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
<VAR>x y : ℂ<GOAL>cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1107598<VAR>N' : Type ?u.1107601<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_8<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>x : LocalizedModule S M₀<GOAL>((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) x = (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1107598<VAR>N' : Type ?u.1107601<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_8<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>x : LocalizedModule S M₀<VAR>m : M₀<VAR>s : ↥S<GOAL>((algebraMap R (Module.End R M₁')) ↑s) (((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s)) = ((algebraMap R (Module.End R M₁')) ↑s) ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1107598<VAR>N' : Type ?u.1107601<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_8<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>x : LocalizedModule S M₀<VAR>m : M₀<VAR>s : ↥S<GOAL>((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) = (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1107598<VAR>N' : Type ?u.1107601<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type u_9<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type u_8<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>x : LocalizedModule S M₀<VAR>m : M₀<VAR>s : ↥S<GOAL>f₁ (g m) = fromLocalizedModule' S f₁ (((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1))
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>hφ : φ.IsSymmetric<VAR>f : R →+* S<VAR>e : Perm σ<GOAL>(rename ⇑e) ((MvPolynomial.map f) φ) = (MvPolynomial.map f) φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>z : at x<GOAL>(stalkToFiberRingHom 𝒜 x) (homogeneousLocalizationToStalk 𝒜 x z) = z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl<GOAL>(stalkToFiberRingHom 𝒜 x) (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) = Quotient.mk'' z
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction₂ X Y<VAR>F : C ⥤ D<VAR>hF : W.IsInvertedBy F<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : F.Additive<GOAL>φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>inst✝² : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction₂ X Y<VAR>F : C ⥤ D<VAR>hF : W.IsInvertedBy F<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : F.Additive<VAR>this : IsIso (F.map φ.s)<GOAL>φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommGroup α<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformGroup α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝¹ : CompleteSpace α<VAR>inst✝ : T2Space α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>s : Finset β<GOAL>(∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommGroup α<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformGroup α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝¹ : CompleteSpace α<VAR>inst✝ : T2Space α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>s : Finset β<GOAL>(∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = (∏' (x : ↑↑s), f ↑x) * ∏' (x : ↑(↑s)ᶜ), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommGroup α<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformGroup α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝¹ : CompleteSpace α<VAR>inst✝ : T2Space α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>s : Finset β<GOAL>∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : ↑(↑s)ᶜ), f ↑x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<VAR>W : C<VAR>k l : t.pt ⟶ W<VAR>h₀ : t.inl ≫ k = t.inl ≫ l<VAR>h₁ : t.inr ≫ k = t.inr ≫ l<GOAL>t.ι.app none ≫ k = t.ι.app none ≫ l
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>(f * g).IsMultiplicative
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>∀ {m n : ℕ}, m.Coprime n → (f * g) (m * n) = (f * g) m * (f * g) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<GOAL>∀ {m n : ℕ}, m.Coprime n → ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 = (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 = (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 = ∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2) = ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, (match a with | ((i, j), k, l) => (i * k, j * l)) ∈ (m * n).divisorsAntidiagonal
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>Set.InjOn (fun x => match x with | ((i, j), k, l) => (i * k, j * l)) ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>Set.SurjOn (fun x => match x with | ((i, j), k, l) => (i * k, j * l)) ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) = f (match a with | ((i, j), k, l) => (i * k, j * l)).1 * g (match a with | ((i, j), k, l) => (i * k, j * l)).2
<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<GOAL>absNorm (span {r}) = ((Algebra.norm ℤ) r).natAbs
<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<GOAL>absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
<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<GOAL>absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
<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 ⋯<GOAL>absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
<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>absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
<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>(LinearMap.det (↑ℤ (Submodule.subtype (span {r})) ∘ₗ (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs