ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_5<VAR>Semiring R<VAR>η : Type u_7<VAR>Fintype η<VAR>M : Type u_9<VAR>ιs : η → Type u_10<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : (j : η) → ιs j →₀ M<VAR>ji : (j : η) × ιs j<GOAL>((Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f) ji = (f ji.fst) ji.snd
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α × β →₀ M<VAR>x : α<VAR>y : β<GOAL>(((Finsupp.finsuppProdLEquiv R) f) x) y = f (x, y)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α →₀ β →₀ M<VAR>xy : α × β<GOAL>((Finsupp.finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>v : α → M<VAR>f : α → R<GOAL>((Fintype.total R S) v) f = ∑ i : α, f i • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>v : α → M<VAR>DecidableEq α<VAR>i : α<VAR>r : R<GOAL>((Fintype.total R S) v) (Pi.single i r) = r • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>v : α → M<VAR>x : α → R<GOAL>(Finsupp.total α M R v) ((Finsupp.linearEquivFunOnFinite R R α).symm x) = ((Fintype.total R S) v) x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>v : α → M<GOAL>Finsupp.total α M R v ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm = (Fintype.total R S) v
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>v : α → M<GOAL>LinearMap.range ((Fintype.total R S) v) = Submodule.span R (Set.range v)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>x : M<GOAL>x ∈ Submodule.span R (Set.range v) ↔ ∃ c, ∑ i : α, c i • v i = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>Fintype α<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<GOAL>⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i : α, c i • v i = x
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>w : Set M<VAR>x : ↥(Submodule.span R w)<GOAL>Span.repr R w x = ⋯.choose
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>w : Set M<VAR>x : ↥(Submodule.span R w)<GOAL>(Finsupp.total (↑w) M R Subtype.val) (Span.repr R w x) = ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>β : Type u_5<VAR>Zero β<VAR>S : Submodule R M<VAR>f : ι →₀ β<VAR>g : ι → β → M<VAR>h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S<GOAL>f.sum g ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>ι : Type u_4<VAR>g : ι → M<VAR>l : ι →₀ R<GOAL>f ((Finsupp.total ι M R g) l) = (Finsupp.total ι N R (⇑f ∘ g)) l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>p : ι → Submodule R M<VAR>m : M<VAR>hm : m ∈ ⨆ i, p i<GOAL>∃ s, m ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>p : ι → Submodule R M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∃ s, m ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set (Submodule R M)<VAR>m : M<GOAL>m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Finset M<VAR>x : M<GOAL>x ∈ Submodule.span R ↑s ↔ ∃ f, ∑ i ∈ s, f i • i = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<VAR>s : Set M<GOAL>m ∈ Submodule.span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<VAR>s : Set M<GOAL>m ∈ Submodule.span R s ↔ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>↑(Submodule.span R s) = ⋃ n, (fun f => ∑ i : Fin n, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>Semiring R<VAR>Subsingleton R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>∀ (x : ι →₀ R), (Module.subsingletonEquiv R M ι).symm x = 0
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>Semiring R<VAR>Subsingleton R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>∀ (x : M), (Module.subsingletonEquiv R M ι) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>f : M →ₗ[R] α →₀ R<VAR>s : Function.Surjective ⇑f<GOAL>f ∘ₗ f.splittingOfFinsuppSurjective s = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>f : M →ₗ[R] α →₀ R<VAR>s : Function.Surjective ⇑f<GOAL>Function.LeftInverse ⇑f ⇑(f.splittingOfFinsuppSurjective s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>f : M →ₗ[R] α →₀ R<VAR>s : Function.Surjective ⇑f<GOAL>Function.Injective ⇑(f.splittingOfFinsuppSurjective s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>Finite α<VAR>f : M →ₗ[R] α → R<VAR>s : Function.Surjective ⇑f<GOAL>f ∘ₗ f.splittingOfFunOnFintypeSurjective s = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>Finite α<VAR>f : M →ₗ[R] α → R<VAR>s : Function.Surjective ⇑f<GOAL>Function.LeftInverse ⇑f ⇑(f.splittingOfFunOnFintypeSurjective s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>Finite α<VAR>f : M →ₗ[R] α → R<VAR>s : Function.Surjective ⇑f<GOAL>Function.Injective ⇑(f.splittingOfFunOnFintypeSurjective s)
<VAR>R : Type u_4<VAR>R₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>ι : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>γ : Type u_9<VAR>Zero γ<VAR>t : ι →₀ γ<VAR>g : ι → γ → M →ₛₗ[σ₁₂] M₂<GOAL>⇑(t.sum g) = ⇑(t.sum fun i d => g i d)
<VAR>R : Type u_4<VAR>R₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>ι : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>γ : Type u_9<VAR>Zero γ<VAR>t : ι →₀ γ<VAR>g : ι → γ → M →ₛₗ[σ₁₂] M₂<VAR>b : M<GOAL>(t.sum g) b = t.sum fun i d => (g i d) b
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>SMulCommClass R S S<VAR>M N : Submodule R S<VAR>ι : Type u_5<VAR>m : ι → ↥M<VAR>n : ι →₀ ↥N<GOAL>(Submodule.mulLeftMap N m) n = n.sum fun i n => ↑(m i) * ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>SMulCommClass R S S<VAR>M N : Submodule R S<VAR>ι : Type u_5<VAR>m : ι → ↥M<VAR>i : ι<VAR>n : ↥N<GOAL>(Submodule.mulLeftMap N m) (Finsupp.single i n) = ↑(m i) * ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>IsScalarTower R S S<VAR>M N : Submodule R S<VAR>ι : Type u_5<VAR>n : ι → ↥N<VAR>m : ι →₀ ↥M<GOAL>(M.mulRightMap n) m = m.sum fun i m => ↑m * ↑(n i)
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>IsScalarTower R S S<VAR>M N : Submodule R S<VAR>ι : Type u_5<VAR>n : ι → ↥N<VAR>i : ι<VAR>m : ↥M<GOAL>(M.mulRightMap n) (Finsupp.single i m) = ↑m * ↑(n i)
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_4<VAR>Semiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>SMulCommClass R S S<VAR>IsScalarTower R S S<VAR>M : Submodule R S<VAR>N : Submodule R S<VAR>ι : Type u_5<VAR>m : ι → ↥M<VAR>hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n<GOAL>Submodule.mulLeftMap N m = N.mulRightMap m
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Module R S<VAR>SMulCommClass R R S<VAR>SMulCommClass R S S<VAR>IsScalarTower R S S<VAR>M : Submodule R S<VAR>N : Submodule R S<VAR>ι : Type u_6<VAR>m : ι → ↥M<GOAL>Submodule.mulLeftMap N m = N.mulRightMap m
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : A<VAR>x : TensorProduct R M N<GOAL>a • x = (LinearMap.rTensor N ((Algebra.lsmul R R M) a)) x
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>f : TensorProduct R M N →ₗ[A] P<VAR>a : M<GOAL>(TensorProduct.AlgebraTensorModule.curry f) a = (TensorProduct.curry (↑R f)) a
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>f : TensorProduct R M N →ₗ[A] P<GOAL>↑R (TensorProduct.AlgebraTensorModule.curry f) = TensorProduct.curry (↑R f)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<GOAL>Function.Injective TensorProduct.AlgebraTensorModule.curry
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>g h : TensorProduct R M N →ₗ[A] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)<GOAL>g = h
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>f : M →ₗ[A] N →ₗ[R] P<VAR>a : TensorProduct R M N<GOAL>(TensorProduct.AlgebraTensorModule.lift f) a = (TensorProduct.lift (↑R f)) a
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>f : M →ₗ[A] N →ₗ[R] P<VAR>x : M<VAR>y : N<GOAL>(TensorProduct.AlgebraTensorModule.lift f) (x ⊗ₜ[R] y) = (f x) y
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>Module B P<VAR>IsScalarTower R A P<VAR>IsScalarTower R B P<VAR>SMulCommClass A B P<VAR>f : M →ₗ[A] N →ₗ[R] P<GOAL>(TensorProduct.AlgebraTensorModule.uncurry R A B M N P) f = TensorProduct.AlgebraTensorModule.lift f
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>Module B P<VAR>IsScalarTower R A P<VAR>IsScalarTower R B P<VAR>SMulCommClass A B P<VAR>f : TensorProduct R M N →ₗ[A] P<GOAL>(TensorProduct.AlgebraTensorModule.lcurry R A B M N P) f = TensorProduct.AlgebraTensorModule.curry f
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>m : M<GOAL>(TensorProduct.AlgebraTensorModule.mk R A M N) m = { toFun := fun x => m ⊗ₜ[R] x, map_add' := ⋯, map_smul' := ⋯ }
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<GOAL>TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>AddCommMonoid P'<VAR>Module R P'<VAR>Module A P'<VAR>IsScalarTower R A P'<VAR>AddCommMonoid Q'<VAR>Module R Q'<VAR>f₂ : P →ₗ[A] P'<VAR>f₁ : M →ₗ[A] P<VAR>g₂ : Q →ₗ[R] Q'<VAR>g₁ : N →ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.AlgebraTensorModule.map f₂ g₂ ∘ₗ TensorProduct.AlgebraTensorModule.map f₁ g₁
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<GOAL>TensorProduct.AlgebraTensorModule.map 1 1 = 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f₁ f₂ : M →ₗ[A] M<VAR>g₁ g₂ : N →ₗ[R] N<GOAL>TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f₁ f₂ : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g = TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M →ₗ[A] P<VAR>g₁ g₂ : N →ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) = TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>r : R<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>Module B P<VAR>IsScalarTower R A P<VAR>IsScalarTower R B P<VAR>SMulCommClass A B P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>b : B<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>Module B P<VAR>IsScalarTower R A P<VAR>IsScalarTower R B P<VAR>SMulCommClass A B P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<GOAL>((TensorProduct.AlgebraTensorModule.mapBilinear R A B M N P Q) f) g = TensorProduct.AlgebraTensorModule.map f g
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>Module B P<VAR>IsScalarTower R A P<VAR>IsScalarTower R B P<VAR>SMulCommClass A B P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<GOAL>(TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<GOAL>TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) = LinearEquiv.refl A (TensorProduct R M N)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>AddCommMonoid P'<VAR>Module R P'<VAR>Module A P'<VAR>IsScalarTower R A P'<VAR>AddCommMonoid Q'<VAR>Module R Q'<VAR>f₁ : M ≃ₗ[A] P<VAR>f₂ : P ≃ₗ[A] P'<VAR>g₁ : N ≃ₗ[R] Q<VAR>g₂ : Q ≃ₗ[R] Q'<GOAL>TensorProduct.AlgebraTensorModule.congr (f₁ ≪≫ₗ f₂) (g₁ ≪≫ₗ g₂) = TensorProduct.AlgebraTensorModule.congr f₁ g₁ ≪≫ₗ TensorProduct.AlgebraTensorModule.congr f₂ g₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M ≃ₗ[A] P<VAR>g : N ≃ₗ[R] Q<GOAL>TensorProduct.AlgebraTensorModule.congr f.symm g.symm = (TensorProduct.AlgebraTensorModule.congr f g).symm
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<GOAL>TensorProduct.AlgebraTensorModule.congr 1 1 = 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f₁ f₂ : M ≃ₗ[A] M<VAR>g₁ g₂ : N ≃ₗ[R] N<GOAL>TensorProduct.AlgebraTensorModule.congr (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.congr f₁ g₁ * TensorProduct.AlgebraTensorModule.congr f₂ g₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M ≃ₗ[A] P<VAR>g : N ≃ₗ[R] Q<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.AlgebraTensorModule.congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>f : M ≃ₗ[A] P<VAR>g : N ≃ₗ[R] Q<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorProduct.AlgebraTensorModule.rid R R M = TensorProduct.rid R M
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>r : R<VAR>m : M<GOAL>(TensorProduct.AlgebraTensorModule.rid R A M) (m ⊗ₜ[R] r) = r • m
<VAR>R : Type uR<VAR>A : Type uA<VAR>M : Type uM<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>m : M<GOAL>(TensorProduct.AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>Algebra A B<VAR>IsScalarTower A B M<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.assoc R A B M P Q) ((m ⊗ₜ[A] p) ⊗ₜ[R] q) = m ⊗ₜ[A] p ⊗ₜ[R] q
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>P : Type uP<VAR>Q : Type uQ<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>AddCommMonoid P<VAR>Module R P<VAR>Module A P<VAR>IsScalarTower R A P<VAR>AddCommMonoid Q<VAR>Module R Q<VAR>Algebra A B<VAR>IsScalarTower A B M<VAR>m : M<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.AlgebraTensorModule.assoc R A B M P Q).symm (m ⊗ₜ[A] p ⊗ₜ[R] q) = (m ⊗ₜ[A] p) ⊗ₜ[R] q