ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>⇑(PiTensorProduct.tprod R) = PiTensorProduct.tprodCoeff R 1
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>z : R<VAR>f : (i : ι) → s i<GOAL>PiTensorProduct.tprodCoeff R z f = z • (PiTensorProduct.tprod R) f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<GOAL>↑p = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>x : PiTensorProduct R fun i => s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<GOAL>p ∈ x.lifts ↔ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>x : PiTensorProduct R fun i => s i<GOAL>x.lifts.Nonempty
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>0 ∈ PiTensorProduct.lifts 0
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>x y : PiTensorProduct R fun i => s i<VAR>p q : FreeAddMonoid (R × ((i : ι) → s i))<VAR>hp : p ∈ x.lifts<VAR>hq : q ∈ y.lifts<GOAL>p + q ∈ (x + y).lifts
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>x : PiTensorProduct R fun i => s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<VAR>h : p ∈ x.lifts<VAR>a : R<GOAL>List.map (fun y => (a * y.1, y.2)) p ∈ (a • x).lifts
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>motive : (PiTensorProduct R fun i => s i) → Prop<VAR>z : PiTensorProduct R fun i => s i<VAR>smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (PiTensorProduct.tprod R) f)<VAR>add : ∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)<GOAL>motive z
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ₁ φ₂ : (PiTensorProduct R fun i => s i) →ₗ[R] E<VAR>H : φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R)<GOAL>φ₁ = φ₂
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>Submodule.span R (Set.range ⇑(PiTensorProduct.tprod R)) = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(PiTensorProduct.liftAux φ) ((PiTensorProduct.tprod R) f) = φ f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>z : R<VAR>f : (i : ι) → s i<GOAL>(PiTensorProduct.liftAux φ) (PiTensorProduct.tprodCoeff R z f) = z • φ f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>r : R<VAR>x : PiTensorProduct R fun i => s i<GOAL>(PiTensorProduct.liftAux φ) (r • x) = r • (PiTensorProduct.liftAux φ) x
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(PiTensorProduct.lift φ) ((PiTensorProduct.tprod R) f) = φ f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E<VAR>H : φ'.compMultilinearMap (PiTensorProduct.tprod R) = φ<GOAL>φ' = PiTensorProduct.lift φ
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ : MultilinearMap R s E<VAR>φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E<VAR>H : ∀ (f : (i : ι) → s i), φ' ((PiTensorProduct.tprod R) f) = φ f<GOAL>φ' = PiTensorProduct.lift φ
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E<GOAL>PiTensorProduct.lift.symm φ' = φ'.compMultilinearMap (PiTensorProduct.tprod R)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>PiTensorProduct.lift (PiTensorProduct.tprod R) = LinearMap.id
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>x : (i : ι) → s i<GOAL>(PiTensorProduct.map f) ((PiTensorProduct.tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>LinearMap.range (PiTensorProduct.map f) = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>(i : ι) → AddCommMonoid (t' i)<VAR>(i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>(PiTensorProduct.map fun i => g i ∘ₗ f i) = PiTensorProduct.map g ∘ₗ PiTensorProduct.map f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>h : MultilinearMap R t E<GOAL>PiTensorProduct.lift h ∘ₗ PiTensorProduct.map f = PiTensorProduct.lift (h.compLinearMap f)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>(PiTensorProduct.map fun i => LinearMap.id) = LinearMap.id
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>(PiTensorProduct.map fun i => 1) = 1
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>f₁ f₂ : (i : ι) → s i →ₗ[R] s i<GOAL>(PiTensorProduct.map fun i => f₁ i * f₂ i) = PiTensorProduct.map f₁ * PiTensorProduct.map f₂
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>f : (i : ι) → s i →ₗ[R] s i<GOAL>PiTensorProduct.mapMonoidHom f = PiTensorProduct.map f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>f : (i : ι) → s i →ₗ[R] s i<VAR>n : ℕ<GOAL>PiTensorProduct.map (f ^ n) = PiTensorProduct.map f ^ n
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>DecidableEq ι<VAR>i : ι<VAR>x : (i : ι) → s i<VAR>u : s i →ₗ[R] t i<GOAL>(fun j => (Function.update f i u j) (x j)) = Function.update (fun j => (f j) (x j)) i (u (x i))
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>DecidableEq ι<VAR>i : ι<VAR>u v : s i →ₗ[R] t i<GOAL>PiTensorProduct.map (Function.update f i (u + v)) = PiTensorProduct.map (Function.update f i u) + PiTensorProduct.map (Function.update f i v)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>DecidableEq ι<VAR>i : ι<VAR>c : R<VAR>u : s i →ₗ[R] t i<GOAL>PiTensorProduct.map (Function.update f i (c • u)) = c • PiTensorProduct.map (Function.update f i u)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>(PiTensorProduct.mapMultilinear R s t) f = PiTensorProduct.map f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>x : (i : ι) → s i<GOAL>(PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f) = PiTensorProduct.map f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i ≃ₗ[R] t i<VAR>m : (i : ι) → s i<GOAL>(PiTensorProduct.congr f) ((PiTensorProduct.tprod R) m) = ⨂ₜ[R] (i : ι), (f i) (m i)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i ≃ₗ[R] t i<VAR>p : (i : ι) → t i<GOAL>(PiTensorProduct.congr f).symm ((PiTensorProduct.tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>(i : ι) → AddCommMonoid (t' i)<VAR>(i : ι) → Module R (t' i)<VAR>f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i<VAR>x : (i : ι) → s i<VAR>y : (i : ι) → t i<GOAL>((PiTensorProduct.map₂ f) ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) = ⨂ₜ[R] (i : ι), ((f i) (x i)) (y i)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>(i : ι) → AddCommMonoid (t' i)<VAR>(i : ι) → Module R (t' i)<VAR>φ ψ : PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i<GOAL>(φ + ψ).piTensorHomMapFun₂ = φ.piTensorHomMapFun₂ + ψ.piTensorHomMapFun₂
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>(i : ι) → AddCommMonoid (t' i)<VAR>(i : ι) → Module R (t' i)<VAR>r : R<VAR>φ : PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i<GOAL>(r • φ).piTensorHomMapFun₂ = r • φ.piTensorHomMapFun₂
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>(i : ι) → AddCommMonoid (t' i)<VAR>(i : ι) → Module R (t' i)<VAR>f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i<VAR>a : (i : ι) → s i<VAR>b : (i : ι) → t i<GOAL>((PiTensorProduct.piTensorHomMap₂ ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) a)) ((PiTensorProduct.tprod R) b) = ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>e : ι ≃ ι₂<VAR>f : (i : ι) → s i<GOAL>(PiTensorProduct.reindex R s e) ((PiTensorProduct.tprod R) f) = (PiTensorProduct.tprod R) fun i => f (e.symm i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>e : ι ≃ ι₂<GOAL>(↑(PiTensorProduct.reindex R s e)).compMultilinearMap (PiTensorProduct.tprod R) = (MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun i => s (e.symm i)) e).symm (PiTensorProduct.tprod R)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>e : ι ≃ ι₂<VAR>φ : MultilinearMap R (fun i => s (e.symm i)) E<GOAL>PiTensorProduct.lift φ ∘ₗ ↑(PiTensorProduct.reindex R s e) = PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>e : ι ≃ ι₂<VAR>φ : MultilinearMap R s E<GOAL>PiTensorProduct.lift φ ∘ₗ ↑(PiTensorProduct.reindex R s e).symm = PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>e : ι ≃ ι₂<VAR>φ : MultilinearMap R (fun i => s (e.symm i)) E<VAR>x : PiTensorProduct R fun i => s i<GOAL>(PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e).symm φ)) x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>E : Type u_9<VAR>AddCommMonoid E<VAR>Module R E<VAR>e : ι ≃ ι₂<VAR>φ : MultilinearMap R s E<VAR>x : PiTensorProduct R fun i => s (e.symm i)<GOAL>(PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e).symm x) = (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)) x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<GOAL>PiTensorProduct.reindex R s e ≪≫ₗ PiTensorProduct.reindex R (fun i => s (e.symm i)) e' = PiTensorProduct.reindex R s (e.trans e')
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>e : ι ≃ ι₂<VAR>e' : ι₂ ≃ ι₃<VAR>x : PiTensorProduct R fun i => s i<GOAL>(PiTensorProduct.reindex R (fun i => s (e.symm i)) e') ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.reindex R s (e.trans e')) x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : ι ≃ ι₂<GOAL>(PiTensorProduct.reindex R (fun x => M) e).symm = PiTensorProduct.reindex R (fun x => M) e.symm
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<GOAL>PiTensorProduct.reindex R s (Equiv.refl ι) = LinearEquiv.refl R (PiTensorProduct R fun i => s i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<GOAL>(PiTensorProduct.map fun i => f (e.symm i)) ∘ₗ ↑(PiTensorProduct.reindex R s e) = ↑(PiTensorProduct.reindex R t e) ∘ₗ PiTensorProduct.map f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<VAR>x : PiTensorProduct R fun i => s i<GOAL>(PiTensorProduct.map fun i => f (e.symm i)) ((PiTensorProduct.reindex R s e) x) = (PiTensorProduct.reindex R t e) ((PiTensorProduct.map f) x)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<GOAL>PiTensorProduct.map f ∘ₗ ↑(PiTensorProduct.reindex R s e).symm = ↑(PiTensorProduct.reindex R t e).symm ∘ₗ PiTensorProduct.map fun i => f (e.symm i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>t : ι → Type u_11<VAR>(i : ι) → AddCommMonoid (t i)<VAR>(i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<VAR>x : PiTensorProduct R fun i => s (e.symm i)<GOAL>(PiTensorProduct.map f) ((PiTensorProduct.reindex R s e).symm x) = (PiTensorProduct.reindex R t e).symm ((PiTensorProduct.map fun i => f (e.symm i)) x)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>IsEmpty ι<VAR>r : R<GOAL>(PiTensorProduct.isEmptyEquiv ι).symm r = r • (PiTensorProduct.tprod R) isEmptyElim
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>IsEmpty ι<VAR>f : (i : ι) → s i<GOAL>(PiTensorProduct.isEmptyEquiv ι) ((PiTensorProduct.tprod R) f) = 1
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton ι<VAR>i₀ : ι<VAR>m : M<GOAL>(PiTensorProduct.subsingletonEquiv i₀).symm m = (PiTensorProduct.tprod R) fun x => m
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton ι<VAR>i : ι<VAR>f : ι → M<GOAL>(PiTensorProduct.subsingletonEquiv i) ((PiTensorProduct.tprod R) f) = f i
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ι → M<VAR>b : ι₂ → M<GOAL>PiTensorProduct.tmul (((PiTensorProduct.tprod R) fun i => a i) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => b i) = (PiTensorProduct.tprod R) fun i => Sum.elim a b i
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ι ⊕ ι₂ → M<GOAL>PiTensorProduct.tmulSymm ((PiTensorProduct.tprod R) fun i => a i) = ((PiTensorProduct.tprod R) fun i => a (Sum.inl i)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => a (Sum.inr i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ι → M<VAR>b : ι₂ → M<GOAL>(PiTensorProduct.tmulEquiv R M) (((PiTensorProduct.tprod R) fun i => a i) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => b i) = (PiTensorProduct.tprod R) fun i => Sum.elim a b i
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ι ⊕ ι₂ → M<GOAL>(PiTensorProduct.tmulEquiv R M).symm ((PiTensorProduct.tprod R) fun i => a i) = ((PiTensorProduct.tprod R) fun i => a (Sum.inl i)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => a (Sum.inr i)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>ι : Type u<VAR>Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hmn : TensorProduct.VanishesTrivially R m n<GOAL>∑ i : ι, m i ⊗ₜ[R] n i = 0
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>ι : Type u<VAR>Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Submodule.span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<GOAL>TensorProduct.VanishesTrivially R m n
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>ι : Type u<VAR>Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Submodule.span R (Set.range m) = ⊤<GOAL>TensorProduct.VanishesTrivially R m n ↔ ∑ i : ι, m i ⊗ₜ[R] n i = 0
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>ι : Type u<VAR>Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<GOAL>TensorProduct.VanishesTrivially R m n
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>ι : Type u<VAR>Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)<GOAL>TensorProduct.VanishesTrivially R m n ↔ ∑ i : ι, m i ⊗ₜ[R] n i = 0
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n<VAR>M' : Submodule R M<GOAL>Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<GOAL>(∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<GOAL>(∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>hMN : ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)<VAR>M' : Submodule R M<GOAL>Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>minpoly R (Matrix.toLin' M) = minpoly R M
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>b : Basis n R N<VAR>M : Matrix n n R<GOAL>minpoly R ((Matrix.toLin b b) M) = minpoly R M