ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Semiring S<VAR>Module S M₂<VAR>SMulCommClass R S M₂<VAR>ι' : Type u_1<VAR>σ : ι ≃ ι'<VAR>f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂<GOAL>(MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ).symm f = { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_add' := ⋯, map_smul' := ⋯ }
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Semiring S<VAR>Module S M₂<VAR>SMulCommClass R S M₂<VAR>IsEmpty ι<VAR>m : M₂<GOAL>(MultilinearMap.constLinearEquivOfIsEmpty R S M₁ M₂) m = MultilinearMap.constOfIsEmpty R M₁ m
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Semiring S<VAR>Module S M₂<VAR>SMulCommClass R S M₂<VAR>IsEmpty ι<VAR>f : MultilinearMap R M₁ M₂<GOAL>(MultilinearMap.constLinearEquivOfIsEmpty R S M₁ M₂).symm f = f 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Semiring S<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>Module S M₃<VAR>SMulCommClass R S M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<GOAL>∀ (a : MultilinearMap R (fun x => M₂) M₃), (MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ) a = (MultilinearMap.domDomCongrEquiv σ).toFun a
<VAR>R : Type uR<VAR>S : Type uS<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Semiring S<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>Module S M₃<VAR>SMulCommClass R S M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<GOAL>∀ (a : MultilinearMap R (fun x => M₂) M₃), (MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ).symm a = (MultilinearMap.domDomCongrEquiv σ).invFun a
<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Set ι<VAR>DecidableEq { x // x ∈ s }<VAR>e : α ≃ ↑s<VAR>m : α → (i : ι) → M₁ i<VAR>a : α<VAR>z : (i : ι) → M₁ i<GOAL>(fun i => Function.update m a z (e.symm i) ↑i) = fun i => Function.update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>M₁' : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (M₁' i)<VAR>(i : ι) → Module R (M₁' i)<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<GOAL>(MultilinearMap.compLinearMapₗ f) g = g.compLinearMap f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>M₁' : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (M₁' i)<VAR>(i : ι) → Module R (M₁' i)<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<GOAL>MultilinearMap.compLinearMapMultilinear f = MultilinearMap.compLinearMapₗ f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>M₁' : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (M₁' i)<VAR>(i : ι) → Module R (M₁' i)<VAR>g : MultilinearMap R M₁' M₂<GOAL>∀ (a : (i : ι) → (fun i => M₁ i →ₗ[R] M₁' i) i) (m : (i : ι) → M₁ i), ((MultilinearMap.piLinearMap g) a) m = g fun i => (a i) (m i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>Fintype ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<GOAL>(f fun i => c i • m i) = (∏ i : ι, c i) • f m
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<GOAL>f (Function.update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (Function.update m i x)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>CommSemiring R<VAR>A : Type u_1<VAR>CommSemiring A<VAR>Algebra R A<VAR>Fintype ι<VAR>m : ι → A<GOAL>(MultilinearMap.mkPiAlgebra R ι A) m = ∏ i : ι, m i
<VAR>R : Type uR<VAR>n : ℕ<VAR>CommSemiring R<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>m : Fin n → A<GOAL>(MultilinearMap.mkPiAlgebraFin R n A) m = (List.ofFn m).prod
<VAR>R : Type uR<VAR>n : ℕ<VAR>CommSemiring R<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>((MultilinearMap.mkPiAlgebraFin R n A) fun x => a) = a ^ n
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ R<VAR>z : M₂<VAR>m : (i : ι) → M₁ i<GOAL>(f.smulRight z) m = f m • z
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<VAR>z : M₂<VAR>m : ι → R<GOAL>(MultilinearMap.mkPiRing R ι z) m = (∏ i : ι, m i) • z
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<VAR>f : MultilinearMap R (fun x => R) M₂<GOAL>MultilinearMap.mkPiRing R ι (f fun x => 1) = f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<VAR>z₁ z₂ : M₂<GOAL>MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<GOAL>MultilinearMap.mkPiRing R ι 0 = 0
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<VAR>z : M₂<GOAL>MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<GOAL>(-f) m = -f m
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f g : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<GOAL>(f - g) m = f m - g m
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x : M₁ i<GOAL>f (Function.update m i (-x)) = -f (Function.update m i x)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x y : M₁ i<GOAL>f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>x : (i : ι) → M₁ i<VAR>i : ι<VAR>v : M₁ i<GOAL>f (Function.update x i v) = f x - f (Function.update x i (x i - v))
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>LinearOrder ι<VAR>a b v : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f (s.piecewise a v) - f (s.piecewise b v) = ∑ i ∈ s, f fun j => if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x h : (i : ι) → M₁ i<GOAL>f (x + h) = f x + (f.linearDeriv x) h + ∑ s ∈ Finset.filter (fun x => 2 ≤ x.card) Finset.univ.powerset, f (s.piecewise h x)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x h h' : (i : ι) → M₁ i<GOAL>f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') = ∑ s ∈ Finset.filter (fun x => 2 ≤ x.card) Finset.univ.powerset, (f (s.piecewise h x) - f (s.piecewise h' x))
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂<VAR>m : (i : Fin n.succ) → M i<GOAL>f.uncurryLeft m = (f (m 0)) (Fin.tail m)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R M M₂<VAR>x : M 0<VAR>m : (i : Fin n) → M i.succ<GOAL>(f.curryLeft x) m = f (Fin.cons x m)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂<GOAL>f.uncurryLeft.curryLeft = f
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R M M₂<GOAL>f.curryLeft.uncurryLeft = f
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)<VAR>m : (i : Fin n.succ) → M i<GOAL>f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.castSucc<VAR>x : M (Fin.last n)<GOAL>(f.curryRight m) x = f (Fin.snoc m x)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)<GOAL>f.uncurryRight.curryRight = f
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>CommSemiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>f : MultilinearMap R M M₂<GOAL>f.curryRight.uncurryRight = f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>ι' : Type u_1<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>u : ι → M'<VAR>v : ι' → M'<GOAL>(f.currySum u) v = f (Sum.elim u v)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>ι' : Type u_1<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>u : ι ⊕ ι' → M'<GOAL>f.uncurrySum u = (f (u ∘ Sum.inl)) (u ∘ Sum.inr)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>ι' : Type u_1<GOAL>⇑(MultilinearMap.currySumEquiv R ι M₂ M' ι') = MultilinearMap.currySum
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>ι' : Type u_1<GOAL>⇑(MultilinearMap.currySumEquiv R ι M₂ M' ι').symm = MultilinearMap.uncurrySum
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>mk : Fin k → M'<VAR>ml : Fin l → M'<GOAL>(((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) mk) ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>m : Fin n → M'<GOAL>((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) m = (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<GOAL>((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) = (f fun x_1 => x) fun x => y
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<GOAL>((f fun x_1 => x) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((sᶜ.orderEmbOfFin hl) i)) = (f fun x_1 => x) fun x => y
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x : M'<GOAL>(((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) fun x_1 => x) = (f fun x_1 => x) fun x_1 => x
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>x y : M'<GOAL>((((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) = f (s.piecewise (fun x_1 => x) fun x => y)
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M' : Type v'<VAR>CommSemiring R<VAR>AddCommMonoid M'<VAR>AddCommMonoid M₂<VAR>Module R M'<VAR>Module R M₂<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>x y : M'<GOAL>(f fun i => Sum.elim (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl).symm i)) = f (s.piecewise (fun x_1 => x) fun x => y)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Ring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Nonempty ι<VAR>f : MultilinearMap R M₁ M₂<VAR>p : (i : ι) → Submodule R (M₁ i)<GOAL>(↑(f.map p)).Nonempty
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>TensorPower.toTensorAlgebra ((PiTensorProduct.tprod R) x) = (TensorAlgebra.tprod R M n) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorPower.toTensorAlgebra GradedMonoid.GOne.one = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i j : ℕ<VAR>a : ⨂[R]^i M<VAR>b : ⨂[R]^j M<GOAL>TensorPower.toTensorAlgebra (GradedMonoid.GMul.mul a b) = TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>TensorPower.toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>TensorAlgebra.ofDirectSum ((DirectSum.of (fun n => ⨂[R]^n M) n) ((PiTensorProduct.tprod R) x)) = (TensorAlgebra.tprod R M n) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>TensorAlgebra.toDirectSum ((TensorAlgebra.ι R) x) = (DirectSum.of (fun n => ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_1 => x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorAlgebra.ofDirectSum.comp TensorAlgebra.toDirectSum = AlgHom.id R (TensorAlgebra R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : TensorAlgebra R M<GOAL>TensorAlgebra.ofDirectSum (TensorAlgebra.toDirectSum x) = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n m : ℕ<VAR>h : n = m<VAR>x : ⨂[R]^n M<GOAL>GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (Equiv.cast ⋯)) x) = GradedMonoid.mk n x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n m : ℕ<VAR>h : n = m<VAR>x : ⨂[R]^n M<GOAL>GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (finCongr h)) x) = GradedMonoid.mk n x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod = GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>TensorAlgebra.toDirectSum ((TensorAlgebra.tprod R M n) x) = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorAlgebra.toDirectSum.comp TensorAlgebra.ofDirectSum = AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : ⨁ (n : ℕ), ⨂[R]^n M<GOAL>TensorAlgebra.toDirectSum (TensorAlgebra.ofDirectSum x) = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : TensorAlgebra R M<GOAL>TensorAlgebra.equivDirectSum a = TensorAlgebra.toDirectSum a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ⨁ (n : ℕ), ⨂[R]^n M<GOAL>TensorAlgebra.equivDirectSum.symm a = TensorAlgebra.ofDirectSum a
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : Module.rank K V < ℵ₀<GOAL>(Basis.ofVectorSpaceIndex K V).Finite
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<GOAL>Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
<VAR>K : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>AddCommGroup V₃<VAR>Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : LinearMap.ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<GOAL>Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → V<VAR>spans : ⊤ ≤ Submodule.span K (Set.range b)<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>LinearIndependent K b
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → V<GOAL>LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → V<GOAL>LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → V<VAR>le_span : ⊤ ≤ Submodule.span K (Set.range b)<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Finset V<VAR>le_span : ⊤ ≤ Submodule.span K ↑s<VAR>card_eq : s.card = FiniteDimensional.finrank K V<GOAL>∀ (a : V), (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ⋯.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>Fintype ↑s<VAR>le_span : ⊤ ≤ Submodule.span K s<VAR>card_eq : s.toFinset.card = FiniteDimensional.finrank K V<GOAL>∀ (a : V), (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ⋯.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)
<VAR>K : Type u<VAR>DivisionRing K<GOAL>max ℵ₀ #K ≤ Module.rank K (ℕ → K)
<VAR>K : Type u<VAR>DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K : Type u<VAR>DivisionRing K<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K : Type u_2<VAR>V : Type u_3<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K : Type u<VAR>DivisionRing K<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Cardinal.lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
<VAR>K : Type u<VAR>DivisionRing K<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>K V : Type u<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V < Module.rank K (V →ₗ[K] K)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<GOAL>(TensorProduct.finsuppLeft R M N ι) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)