ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.592608<VAR>Bₘ : Type ?u.592611<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(intNorm A B) 0 = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.592608<VAR>Bₘ : Type ?u.592611<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(intNorm A B) 0 = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.592608<VAR>Bₘ : Type ?u.592611<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(intNorm A B) 0 = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.592608<VAR>Bₘ : Type ?u.592611<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) 0) = (algebraMap A (FractionRing A)) 0
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P✝ : Ideal S<VAR>P_prime✝ : P✝.IsPrime<VAR>hP✝ : P✝ ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>a b : S<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>ab_mem : a * b ∈ P ^ (i + 1)<GOAL>b ∈ P
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P✝ : Ideal S<VAR>P_prime✝ : P✝.IsPrime<VAR>hP✝ : P✝ ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>a b : S<VAR>a_not_mem : ¬P ^ i * P ∣ span {a}<VAR>ab_mem : P ^ i * P ∣ span {a} * span {b}<GOAL>P ∣ span {b}
<VAR>n : ℕ<GOAL>2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
<VAR>n : ℕ<GOAL>(n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>φ : R[X] →ₐ[R] A<VAR>p : R[X]<GOAL>φ p = eval₂ (algebraMap R A) (φ X) p
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.card • b < ↑s.card<GOAL>∃ y ∈ t, b < ↑(filter (fun x => f x = y) s).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.card • b < ∑ a ∈ s, 1<GOAL>∃ y ∈ t, b < ∑ a ∈ filter (fun x => f x = y) s, 1
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : X → A<VAR>x : X<GOAL>((lift R) f) (ι R x) = f x
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : X → A<VAR>x : X<GOAL>({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f) (Quot.mk (Rel R X) (Pre.of x)) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>x y : ℚ<VAR>hxy : x ≤ y<VAR>h_1 : x < 0<VAR>h_2 : y < 0<GOAL>0 ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>x y : ℚ<VAR>hxy : x ≤ y<VAR>h_1 : x < 0<VAR>h_2 : ¬y < 0<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>x y : ℚ<VAR>hxy : x ≤ y<VAR>h_1 : ¬x < 0<VAR>h_2 : y < 0<GOAL>1 ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>x y : ℚ<VAR>hxy : x ≤ y<VAR>h_1 : ¬x < 0<VAR>h_2 : ¬y < 0<GOAL>1 ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>xs ys : List α<VAR>ls : List (List α)<VAR>f : List α → List α<VAR>h : ∀ (x : α), x ∈ xs → ¬p x = true<VAR>sep : α<VAR>hsep : p sep = true<VAR>as : List α<GOAL>splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(auxEquiv R 𝒜 ℬ).symm (((gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) (a₁ ᵍ⊗ₜ[R] ↑b₁))) ((auxEquiv R 𝒜 ℬ) (↑a₂ ᵍ⊗ₜ[R] b₂))) = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ).symm.symm ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm (((gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (decompose ℬ) ↑b₁)) ((decompose 𝒜) ↑a₂ ⊗ₜ[R] (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ).symm.symm ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm (((gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (DirectSum.of (fun i => ↥(ℬ i)) j₁) b₁)) ((DirectSum.of (fun i => ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ).symm.symm ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm (((gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (lof R ι (fun i => ↥(ℬ i)) j₁) b₁)) ((lof R ι (fun i => ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ).symm.symm ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm ((-1) ^ (j₁ * i₂) • ((decompose 𝒜) a₁ * (lof R ι (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] ((lof R ι (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ).symm.symm ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm ((-1) ^ (j₁ * i₂) • ((decompose 𝒜) a₁ * (DirectSum.of (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] ((DirectSum.of (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(of R 𝒜 ℬ) ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm ((-1) ^ (j₁ * i₂) • ((decompose 𝒜) a₁ * (DirectSum.of (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] ((DirectSum.of (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((TensorProduct.congr (decomposeAlgEquiv 𝒜).toLinearEquiv (decomposeAlgEquiv ℬ).toLinearEquiv).symm (((decompose 𝒜) a₁ * (DirectSum.of (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] ((DirectSum.of (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂))) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((decomposeAlgEquiv 𝒜).toLinearEquiv.symm ((decompose 𝒜) a₁ * (DirectSum.of (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] (decomposeAlgEquiv ℬ).toLinearEquiv.symm ((DirectSum.of (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂)) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>(-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((decompose 𝒜).symm ((decompose 𝒜) a₁ * (DirectSum.of (fun x => ↥(𝒜 x)) i₂) a₂) ⊗ₜ[R] (decompose ℬ).symm ((DirectSum.of (fun x => ↥(ℬ x)) j₁) b₁ * (decompose ℬ) b₂)) = (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f x < f (a • x + b • y)<GOAL>f (a • x + b • y) < f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : b + a = 1<VAR>hfx : f x < f (b • y + a • x)<GOAL>f (b • y + a • x) < f y
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type u<VAR>hf : ∀ (j : J), Finite (F.obj j)<VAR>hne : ∀ (j : J), Nonempty (F.obj j)<VAR>F' : J ⥤ TopCat := F ⋙ TopCat.discrete<VAR>this✝¹ : ∀ (j : J), DiscreteTopology ↑(F'.obj j)<VAR>this✝ : ∀ (j : J), Finite ↑(F'.obj j)<VAR>this : ∀ (j : J), Nonempty ↑(F'.obj j)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type u<VAR>hf : ∀ (j : J), Finite (F.obj j)<VAR>hne : ∀ (j : J), Nonempty (F.obj j)<VAR>F' : J ⥤ TopCat := F ⋙ TopCat.discrete<VAR>this✝¹ : ∀ (j : J), DiscreteTopology ↑(F'.obj j)<VAR>this✝ : ∀ (j : J), Finite ↑(F'.obj j)<VAR>this : ∀ (j : J), Nonempty ↑(F'.obj j)<VAR>u : (j : J) → ↑(F'.obj j)<VAR>hu : u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (F'.map f) (u i) = u j}<GOAL>F.sections.Nonempty
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>η a ⟂ₘ (κ.singularPart η) a
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsEmpty n<VAR>A : Matrix n n R<GOAL>A.det = 1
<VAR>m n k : ℕ<GOAL>m.gcd (n + m * k) = m.gcd n
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>I J K : Submodule R A<GOAL>I ≤ J / K ↔ I * K ≤ J
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : ↥T†.domain<GOAL>(if hT : Dense ↑T.domain then adjointAux hT else 0) y = (adjointAux hT) y
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<VAR>this : Nontrivial R<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<VAR>this✝ : Nontrivial R<VAR>this : Finite ι<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<VAR>this✝ : Nontrivial R<VAR>this : Finite ι<VAR>val✝ : Fintype ι<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<VAR>this✝ : Nontrivial R<VAR>this : Finite ι<VAR>val✝ : Fintype ι<GOAL>↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>inst✝ : Fintype ↑w<VAR>s : span R w = ⊤<VAR>this✝ : Nontrivial R<VAR>this : Finite ι<VAR>val✝ : Fintype ι<GOAL>Fintype.card ι ≤ Fintype.card ↑w
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>f : Ω → Ω'<VAR>c : ℝ≥0<VAR>ν : FiniteMeasure Ω<VAR>s : Set Ω'<VAR>a✝ : MeasurableSet s<GOAL>↑((c • ν).map f) s = ↑(c • ν.map f) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a x✝¹ x✝ : α<GOAL>x✝¹ ⊓ x✝ = a → x✝¹ = a ∨ x✝ = a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω => (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᶠ[ae μ] fun ω => (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(bliminf u f fun x => True) = liminf u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(p * C a).natDegree = p.natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a✝ b✝ c d a b : K<VAR>h : b ≠ 0<GOAL>(a - b) / b = a / b - 1