ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<VAR>hv : Submodule.span R s = ⊤<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>ι : Sort u_9<VAR>v : ι → M<VAR>f g : F<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>h : ∀ (i : ι), f (v i) = g (v i)<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<GOAL>LinearMap.ker (LinearMap.toSpanSingleton R M x) = ⊥
<VAR>K : Type u_3<VAR>V : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : V →ₗ[K] K<VAR>x : V<VAR>hx : f x ≠ 0<GOAL>Submodule.span K {x} ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<VAR>t : R<GOAL>(LinearEquiv.toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<GOAL>(LinearEquiv.toSpanNonzeroSingleton R M x h) 1 = ⟨x, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<GOAL>(LinearEquiv.coord R M x h) ⟨x, ⋯⟩ = 1
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>h : x ≠ 0<VAR>y : ↥(Submodule.span R {x})<GOAL>(LinearEquiv.coord R M x h) y • x = ↑y
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.intDegree 0 = 0
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.intDegree 1 = 0
<VAR>K : Type u<VAR>Field K<VAR>k : K<GOAL>(RatFunc.C k).intDegree = 0
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.X.intDegree = 1
<VAR>K : Type u<VAR>Field K<VAR>p : Polynomial K<GOAL>((algebraMap (Polynomial K) (RatFunc K)) p).intDegree = ↑p.natDegree
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).intDegree = x.intDegree + y.intDegree
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>(-x).intDegree = x.intDegree
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<VAR>hxy : x + y ≠ 0<GOAL>(x + y).intDegree = ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<VAR>hx : x ≠ 0<VAR>s : Polynomial K<VAR>hs : s ≠ 0<GOAL>↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<GOAL>(x + y).intDegree ≤ max x.intDegree y.intDegree
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>motive : TensorProduct R M N → Prop<VAR>z : TensorProduct R M N<VAR>zero : motive 0<VAR>tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)<VAR>add : ∀ (x y : TensorProduct R M N), motive x → motive y → motive (x + y)<GOAL>motive z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>f : M →+ N →+ P<VAR>hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>n : N<GOAL>0 ⊗ₜ[R] n = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m₁ m₂ : M<VAR>n : N<GOAL>(m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<GOAL>m ⊗ₜ[R] 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n₁ n₂ : N<GOAL>m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>DistribMulAction R' N<VAR>self : TensorProduct.CompatibleSMul R R' M N<VAR>r : R'<VAR>m : M<VAR>n : N<GOAL>(r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>DistribMulAction R' N<VAR>TensorProduct.CompatibleSMul R R' M N<VAR>r : R'<VAR>m : M<VAR>n : N<GOAL>(r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>R' : Type u_10<VAR>SMul R' M<VAR>r : R'<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>SMulCommClass R R' M<VAR>r : R'<GOAL>r • 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>SMulCommClass R R' M<VAR>r : R'<VAR>x y : TensorProduct R M N<GOAL>r • (x + y) = r • x + r • y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R'' : Type u_3<VAR>Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module R'' M<VAR>SMulCommClass R R'' M<VAR>x : TensorProduct R M N<GOAL>0 • x = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>SMulCommClass R R' M<VAR>x : TensorProduct R M N<GOAL>1 • x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R'' : Type u_3<VAR>Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module R'' M<VAR>SMulCommClass R R'' M<VAR>r s : R''<VAR>x : TensorProduct R M N<GOAL>(r + s) • x = r • x + s • x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>SMulCommClass R R' M<VAR>r : R'<VAR>m : M<VAR>n : N<GOAL>r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R' : Type u_2<VAR>Monoid R'<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>DistribMulAction R' M<VAR>SMulCommClass R R' M<VAR>DistribMulAction R' N<VAR>TensorProduct.CompatibleSMul R R' M N<VAR>r : R'<VAR>x : M<VAR>y : N<GOAL>x ⊗ₜ[R] (r • y) = r • x ⊗ₜ[R] y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>r s : R<VAR>m : M<VAR>n : N<GOAL>(r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.mk R M N) m) n = m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x₁ : M<VAR>x₂ : N<VAR>P : Prop<VAR>Decidable P<GOAL>(if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x₁ : M<VAR>x₂ : N<VAR>P : Prop<VAR>Decidable P<GOAL>(x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>α : Type u_10<VAR>s : Finset α<VAR>m : α → M<VAR>n : N<GOAL>(∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>α : Type u_10<VAR>s : Finset α<VAR>n : α → N<GOAL>m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>Submodule.map₂ (TensorProduct.mk R M N) ⊤ ⊤ = ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : TensorProduct R M N<VAR>h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n<GOAL>∃ m n, x = m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.liftAux f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>r : R<VAR>x : TensorProduct R M N<GOAL>(TensorProduct.liftAux f) (r • x) = r • (TensorProduct.liftAux f) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>x : M<VAR>y : N<GOAL>(TensorProduct.lift f) (x ⊗ₜ[R] y) = (f x) y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>x : M<VAR>y : N<GOAL>(TensorProduct.lift f).toAddHom (x ⊗ₜ[R] y) = (f x) y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>g h : TensorProduct R M N →ₗ[R] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)<GOAL>g = h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g : TensorProduct R M N →ₗ[R] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y<GOAL>g = TensorProduct.lift f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>TensorProduct.lift (TensorProduct.mk R M N) = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g : P →ₗ[R] Q<GOAL>TensorProduct.lift (f.compr₂ g) = g ∘ₗ TensorProduct.lift f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : TensorProduct R M N →ₗ[R] P<GOAL>TensorProduct.lift ((TensorProduct.mk R M N).compr₂ f) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>g h : TensorProduct R M N →ₗ[R] P<VAR>H : (TensorProduct.mk R M N).compr₂ g = (TensorProduct.mk R M N).compr₂ h<GOAL>g = h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.lift.equiv R M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : TensorProduct R M N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(((TensorProduct.lift.equiv R M N P).symm f) m) n = f (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : TensorProduct R M N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(((TensorProduct.lcurry R M N P) f) m) n = f (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : TensorProduct R M N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.curry f) m) n = f (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<GOAL>Function.Injective TensorProduct.curry
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g h : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q<VAR>H : ∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)<GOAL>g = h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>g h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₗ[R] S<VAR>H : ∀ (w : M) (x : N) (y : P) (z : Q), g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)<GOAL>g = h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S<VAR>H : ∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<VAR>r : R<GOAL>(TensorProduct.lid R M) (r ⊗ₜ[R] m) = r • m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(TensorProduct.lid R M).symm m = 1 ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.comm R M N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.comm R M N).symm (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<GOAL>TensorProduct.lift f ∘ₗ ↑(TensorProduct.comm R N M) = TensorProduct.lift f.flip
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<VAR>r : R<GOAL>(TensorProduct.rid R M) (m ⊗ₜ[R] r) = r • m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(TensorProduct.rid R M).symm m = m ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>TensorProduct.lid R R = TensorProduct.rid R R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>m : M<VAR>n : N<VAR>p : P<GOAL>(TensorProduct.assoc R M N P) ((m ⊗ₜ[R] n) ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>m : M<VAR>n : N<VAR>p : P<GOAL>(TensorProduct.assoc R M N P).symm (m ⊗ₜ[R] n ⊗ₜ[R] p) = (m ⊗ₜ[R] n) ⊗ₜ[R] p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.map f g ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R Q P) ∘ₗ TensorProduct.map g f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>x : TensorProduct R N M<GOAL>(TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R Q P) ((TensorProduct.map g f) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M →ₗ[R] Q<VAR>g : N →ₗ[R] S<VAR>h : P →ₗ[R] T<GOAL>TensorProduct.map f (TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) = ↑(TensorProduct.assoc R Q S T) ∘ₗ TensorProduct.map (TensorProduct.map f g) h
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M →ₗ[R] Q<VAR>g : N →ₗ[R] S<VAR>h : P →ₗ[R] T<VAR>x : TensorProduct R (TensorProduct R M N) P<GOAL>(TensorProduct.map f (TensorProduct.map g h)) ((TensorProduct.assoc R M N P) x) = (TensorProduct.assoc R Q S T) ((TensorProduct.map (TensorProduct.map f g) h) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M →ₗ[R] Q<VAR>g : N →ₗ[R] S<VAR>h : P →ₗ[R] T<GOAL>TensorProduct.map (TensorProduct.map f g) h ∘ₗ ↑(TensorProduct.assoc R M N P).symm = ↑(TensorProduct.assoc R Q S T).symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M →ₗ[R] Q<VAR>g : N →ₗ[R] S<VAR>h : P →ₗ[R] T<VAR>x : TensorProduct R M (TensorProduct R N P)<GOAL>(TensorProduct.map (TensorProduct.map f g) h) ((TensorProduct.assoc R M N P).symm x) = (TensorProduct.assoc R Q S T).symm ((TensorProduct.map f (TensorProduct.map g h)) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>LinearMap.range (TensorProduct.map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R P<VAR>Module R Q<VAR>p : Submodule R P<VAR>q : Submodule R Q<GOAL>LinearMap.range (TensorProduct.mapIncl p q) = Submodule.span R (Set.image2 (fun x x_1 => x ⊗ₜ[R] x_1) ↑p ↑q)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>f : P →ₗ[R] Q →ₗ[R] M<VAR>p : Submodule R P<VAR>q : Submodule R Q<GOAL>Submodule.map₂ f p q = LinearMap.range (TensorProduct.lift f ∘ₗ TensorProduct.mapIncl p q)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>AddCommMonoid P'<VAR>Module R P'<VAR>AddCommMonoid Q'<VAR>Module R Q'<VAR>f₂ : P →ₗ[R] P'<VAR>f₁ : M →ₗ[R] P<VAR>g₂ : Q →ₗ[R] Q'<VAR>g₁ : N →ₗ[R] Q<GOAL>TensorProduct.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.map f₂ g₂ ∘ₗ TensorProduct.map f₁ g₁
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R P<VAR>Module R Q<VAR>p p' : Submodule R P<VAR>q q' : Submodule R Q<VAR>hp : p ≤ p'<VAR>hq : q ≤ q'<GOAL>LinearMap.range (TensorProduct.mapIncl p q) ≤ LinearMap.range (TensorProduct.mapIncl p' q')
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Q' : Type u_11<VAR>AddCommMonoid Q'<VAR>Module R Q'<VAR>i : P →ₗ[R] Q →ₗ[R] Q'<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.lift i ∘ₗ TensorProduct.map f g = TensorProduct.lift ((i ∘ₗ f).compl₂ g)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>TensorProduct.map 1 1 = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f₁ f₂ : M →ₗ[R] M<VAR>g₁ g₂ : N →ₗ[R] N<GOAL>TensorProduct.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.map f₁ g₁ * TensorProduct.map f₂ g₂