ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra S C<VAR>f : A ⊗[R] B ≃ₗ[S] C<VAR>h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)<VAR>h_one : f (1 ⊗ₜ[R] 1) = 1<VAR>x : A ⊗[R] B<GOAL>(Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct f h_mul h_one) x = f x
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : (A ⊗[R] B) ⊗[R] C ≃ₗ[R] D<VAR>h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), f (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = f ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * f ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)<VAR>h_one : f ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1<VAR>x : (A ⊗[R] B) ⊗[R] C<GOAL>(Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct f h_mul h_one) x = f x
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f : A →ₐ[S] C<VAR>g : B →ₐ[R] C<VAR>hfg : ∀ (x : A) (y : B), Commute (f x) (g y)<VAR>a : A<VAR>b : B<GOAL>(Algebra.TensorProduct.lift f g hfg) (a ⊗ₜ[R] b) = f a * g b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<GOAL>Algebra.TensorProduct.lift Algebra.TensorProduct.includeLeft Algebra.TensorProduct.includeRight ⋯ = AlgHom.id S (A ⊗[R] B)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f : A →ₐ[S] C<VAR>g : B →ₐ[R] C<VAR>hfg : ∀ (x : A) (y : B), Commute (f x) (g y)<GOAL>(Algebra.TensorProduct.lift f g hfg).comp Algebra.TensorProduct.includeLeft = f
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f : A →ₐ[S] C<VAR>g : B →ₐ[R] C<VAR>hfg : ∀ (x : A) (y : B), Commute (f x) (g y)<GOAL>(AlgHom.restrictScalars R (Algebra.TensorProduct.lift f g hfg)).comp Algebra.TensorProduct.includeRight = g
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }<GOAL>Algebra.TensorProduct.liftEquiv fg = Algebra.TensorProduct.lift (↑fg).1 (↑fg).2 ⋯
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>f' : A ⊗[R] B →ₐ[S] C<GOAL>↑(Algebra.TensorProduct.liftEquiv.symm f') = (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(Algebra.TensorProduct.lid R A).toLinearEquiv = TensorProduct.lid R A
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>a : A<GOAL>(Algebra.TensorProduct.lid R A) (r ⊗ₜ[R] a) = r • a
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>(Algebra.TensorProduct.lid R A).symm a = 1 ⊗ₜ[R] a
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<GOAL>(Algebra.TensorProduct.rid R S A).toLinearEquiv = TensorProduct.AlgebraTensorModule.rid R S A
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>r : R<VAR>a : A<GOAL>(Algebra.TensorProduct.rid R S A) (a ⊗ₜ[R] r) = r • a
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : A<GOAL>(Algebra.TensorProduct.rid R S A).symm a = a ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<GOAL>(Algebra.TensorProduct.comm R A B).toLinearEquiv = TensorProduct.comm R A B
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>a : A<VAR>b : B<GOAL>(Algebra.TensorProduct.comm R A B) (a ⊗ₜ[R] b) = b ⊗ₜ[R] a
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>a : A<VAR>b : B<GOAL>(Algebra.TensorProduct.comm R A B).symm (b ⊗ₜ[R] a) = a ⊗ₜ[R] b
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<GOAL>(Algebra.TensorProduct.comm R A B).symm = Algebra.TensorProduct.comm R B A
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<GOAL>Algebra.adjoin R {t | ∃ a b, a ⊗ₜ[R] b = t} = ⊤
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>a₁ a₂ : A<VAR>b₁ b₂ : B<VAR>c₁ c₂ : C<GOAL>(TensorProduct.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) = (TensorProduct.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * (TensorProduct.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<GOAL>(TensorProduct.assoc R A B C) ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<GOAL>(Algebra.TensorProduct.assoc R A B C).toLinearEquiv = TensorProduct.assoc R A B C
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>a : A<VAR>b : B<VAR>c : C<GOAL>(Algebra.TensorProduct.assoc R A B C) ((a ⊗ₜ[R] b) ⊗ₜ[R] c) = a ⊗ₜ[R] b ⊗ₜ[R] c
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>a : A<VAR>b : B<VAR>c : C<GOAL>(Algebra.TensorProduct.assoc R A B C).symm (a ⊗ₜ[R] b ⊗ₜ[R] c) = (a ⊗ₜ[R] b) ⊗ₜ[R] c
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A →ₐ[S] B<VAR>g : C →ₐ[R] D<VAR>a : A<VAR>c : C<GOAL>(Algebra.TensorProduct.map f g) (a ⊗ₜ[R] c) = f a ⊗ₜ[R] g c
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring C<VAR>Algebra R C<GOAL>Algebra.TensorProduct.map (AlgHom.id S A) (AlgHom.id R C) = AlgHom.id S (A ⊗[R] C)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>Semiring D<VAR>Algebra R D<VAR>Semiring E<VAR>Algebra R E<VAR>Semiring F<VAR>Algebra R F<VAR>f₂ : B →ₐ[S] C<VAR>f₁ : A →ₐ[S] B<VAR>g₂ : E →ₐ[R] F<VAR>g₁ : D →ₐ[R] E<GOAL>Algebra.TensorProduct.map (f₂.comp f₁) (g₂.comp g₁) = (Algebra.TensorProduct.map f₂ g₂).comp (Algebra.TensorProduct.map f₁ g₁)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A →ₐ[S] B<VAR>g : C →ₐ[R] D<GOAL>(Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeLeft.comp f
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A →ₐ[S] B<VAR>g : C →ₐ[R] D<GOAL>(AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp g
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<GOAL>(Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp g
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<GOAL>(Algebra.TensorProduct.map f g).range = (Algebra.TensorProduct.includeLeft.comp f).range ⊔ (Algebra.TensorProduct.includeRight.comp g).range
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A ≃ₐ[S] B<VAR>g : C ≃ₐ[R] D<GOAL>(Algebra.TensorProduct.congr f g).toLinearEquiv = TensorProduct.AlgebraTensorModule.congr f.toLinearEquiv g.toLinearEquiv
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A ≃ₐ[S] B<VAR>g : C ≃ₐ[R] D<VAR>x : A ⊗[R] C<GOAL>(Algebra.TensorProduct.congr f g) x = (Algebra.TensorProduct.map ↑f ↑g) x
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A ≃ₐ[S] B<VAR>g : C ≃ₐ[R] D<VAR>x : B ⊗[R] D<GOAL>(Algebra.TensorProduct.congr f g).symm x = (Algebra.TensorProduct.map ↑f.symm ↑g.symm) x
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring C<VAR>Algebra R C<GOAL>Algebra.TensorProduct.congr AlgEquiv.refl AlgEquiv.refl = AlgEquiv.refl
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Algebra S C<VAR>IsScalarTower R S C<VAR>Semiring D<VAR>Algebra R D<VAR>Semiring E<VAR>Algebra R E<VAR>Semiring F<VAR>Algebra R F<VAR>f₁ : A ≃ₐ[S] B<VAR>f₂ : B ≃ₐ[S] C<VAR>g₁ : D ≃ₐ[R] E<VAR>g₂ : E ≃ₐ[R] F<GOAL>Algebra.TensorProduct.congr (f₁.trans f₂) (g₁.trans g₂) = (Algebra.TensorProduct.congr f₁ g₁).trans (Algebra.TensorProduct.congr f₂ g₂)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>f : A ≃ₐ[S] B<VAR>g : C ≃ₐ[R] D<GOAL>Algebra.TensorProduct.congr f.symm g.symm = (Algebra.TensorProduct.congr f g).symm
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>(Algebra.TensorProduct.lmul' R).toLinearMap = LinearMap.mul' R S
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>a b : S<GOAL>(Algebra.TensorProduct.lmul' R) (a ⊗ₜ[R] b) = a * b
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>(Algebra.TensorProduct.lmul' R).comp Algebra.TensorProduct.includeLeft = AlgHom.id R S
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>(Algebra.TensorProduct.lmul' R).comp Algebra.TensorProduct.includeRight = AlgHom.id R S
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<GOAL>Algebra.TensorProduct.productMap f g = (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<VAR>a : A<VAR>b : B<GOAL>(Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] b) = f a * g b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<VAR>a : A<GOAL>(Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] 1) = f a
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<GOAL>(Algebra.TensorProduct.productMap f g).comp Algebra.TensorProduct.includeLeft = f
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<VAR>b : B<GOAL>(Algebra.TensorProduct.productMap f g) (1 ⊗ₜ[R] b) = g b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<GOAL>(Algebra.TensorProduct.productMap f g).comp Algebra.TensorProduct.includeRight = g
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>CommSemiring S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<GOAL>(Algebra.TensorProduct.productMap f g).range = f.range ⊔ g.range
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>m : M<GOAL>(Algebra.TensorProduct.basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>x : A ⊗[R] M<GOAL>(Algebra.TensorProduct.basisAux A b) (a • x) = a • (Algebra.TensorProduct.basisAux A b) x
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>m : M<GOAL>(Algebra.TensorProduct.basis A b).repr (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>i : ι<GOAL>(Algebra.TensorProduct.basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>(Algebra.TensorProduct.basis A b) i = 1 ⊗ₜ[R] b i
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>i : ι<GOAL>a • (Algebra.TensorProduct.basis A b) i = a ⊗ₜ[R] b i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>AddCommMonoid N<VAR>Module R N<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<GOAL>LinearMap.baseChange A ((b'.linearMap b) ij) = ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>ij : ι × ι<GOAL>LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι : Type u_4<VAR>ι₂ : Type u_5<VAR>A : Type u_6<VAR>Fintype ι<VAR>Finite ι₂<VAR>DecidableEq ι<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>b₁ : Basis ι R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>(LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)) (LinearMap.baseChange A f) = ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<GOAL>∀ (a : A ⊗[R] (M →ₗ[R] N)), (LinearMap.tensorProduct R A M N) a = (TensorProduct.liftAux (↑R { toFun := fun a => a • LinearMap.baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ })) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>AddCommGroup M<VAR>Module R M<VAR>a : A ⊗[R] Module.End R M<GOAL>(LinearMap.tensorProductEnd R A M) a = (TensorProduct.liftAux (↑R { toFun := fun a => a • LinearMap.baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ })) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>Module R M<VAR>Module S M<VAR>Module A M<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower S A M<VAR>IsScalarTower R S M<VAR>f : Module.End A M<VAR>g : Module.End R N<GOAL>Module.endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>Algebra K L<VAR>E1 E2 : Subalgebra K L<VAR>Module.Finite K ↥E1<VAR>Module.Finite K ↥E2<GOAL>Module.Finite K ↥(E1 ⊔ E2)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CommRing L<VAR>Algebra K L<VAR>E1 E2 : Subalgebra K L<VAR>FiniteDimensional K ↥E1<VAR>FiniteDimensional K ↥E2<GOAL>FiniteDimensional K ↥(E1 ⊔ E2)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>a : A<VAR>b : B<VAR>m : M<GOAL>(TensorProduct.Algebra.moduleAux (a ⊗ₜ[R] b)) m = a • b • m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring A<VAR>Semiring B<VAR>Module A M<VAR>Module B M<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>a : A<VAR>b : B<VAR>m : M<GOAL>a ⊗ₜ[R] b • m = a • b • m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>f : R →+* S<VAR>x : R<GOAL>f.IsIntegralElem (f x)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>x : R<GOAL>IsIntegral R ((algebraMap R A) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_5<VAR>C : Type u_6<VAR>F : Type u_7<VAR>Ring B<VAR>Ring C<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra R C<VAR>IsScalarTower R A B<VAR>Algebra A C<VAR>IsScalarTower R A C<VAR>b : B<VAR>FunLike F B C<VAR>AlgHomClass F A B C<VAR>f : F<VAR>hb : IsIntegral R b<GOAL>IsIntegral R (f b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>x : A<GOAL>IsIntegral R (f x) ↔ IsIntegral R x
<VAR>R : Type u_5<VAR>A : Type u_6<VAR>CommRing R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (Polynomial.aeval x) f = 0<GOAL>Submodule.span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>hx : IsIntegral R x<GOAL>(Subalgebra.toSubmodule (Algebra.adjoin R {x})).FG
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>f : R →+* B<GOAL>f.IsIntegralElem 0
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<GOAL>IsIntegral R 0
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>f : R →+* B<GOAL>f.IsIntegralElem 1
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<GOAL>IsIntegral R 1
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : IsIntegral R (x ^ n)<GOAL>IsIntegral R x
<VAR>A : Type u_1<VAR>R : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>self : IsIntegralClosure A R B<VAR>x : B<GOAL>IsIntegral R x ↔ ∃ y, (algebraMap A B) y = x
<VAR>A : Type u_1<VAR>R : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>self : IsIntegralClosure A R B<GOAL>Function.Injective ⇑(algebraMap A B)
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>Zero R<VAR>One R<VAR>a : Γ<GOAL>HahnSeries.coeff 1 a = if a = 0 then 1 else 0