ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>StrongRankCondition R<VAR>v : M<VAR>n : v ≠ 0<VAR>h : ∀ (w : M), ∃ c, c • v = w<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>StrongRankCondition R<VAR>v : M<VAR>n : v ≠ 0<VAR>h : ∀ (w : M), ∃ c, c • v = w<GOAL>FiniteDimensional.finrank R M = 1
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>StrongRankCondition R<VAR>v : M<VAR>h : ∀ (w : M), ∃ c, c • v = w<GOAL>FiniteDimensional.finrank R M ≤ 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(TensorAlgebra.GradedAlgebra.ι R M) m = (DirectSum.of (fun i => ↥(LinearMap.range (TensorAlgebra.ι R) ^ i)) 1) ⟨(TensorAlgebra.ι R) 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>self : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x y : M₁ i<GOAL>self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (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 : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>self : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<GOAL>self.toFun (Function.update m i (c • x)) = c • self.toFun (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 : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<GOAL>f.toFun = ⇑f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : ((i : ι) → M₁ i) → M₂<VAR>h₁ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)<VAR>h₂ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c • x)) = c • f (Function.update m i x)<GOAL>⇑{ toFun := f, map_add' := h₁, map_smul' := h₂ } = f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f g : MultilinearMap R M₁ M₂<VAR>h : f = g<VAR>x : (i : ι) → M₁ i<GOAL>f x = g x
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>x y : (i : ι) → M₁ i<VAR>h : x = y<GOAL>f x = f y
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f g : MultilinearMap R M₁ M₂<GOAL>⇑f = ⇑g ↔ f = g
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>H : ∀ (x : (i : ι) → M₁ i), f x = f' x<GOAL>f = f'
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f g : MultilinearMap R M₁ M₂<GOAL>f = g ↔ ∀ (x : (i : ι) → M₁ i), f x = g x
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>h₁ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)<VAR>h₂ : ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c • x)) = c • f (Function.update m i x)<GOAL>{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } = f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>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 : ι) → 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>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<GOAL>f (Function.update m i (c • x)) = c • 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 : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>h : m i = 0<GOAL>f m = 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>AddCommMonoid 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 : ι<GOAL>f (Function.update m i 0) = 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>Nonempty ι<GOAL>f 0 = 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<GOAL>(f + f') m = 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>m : (i : ι) → M₁ i<GOAL>0 m = 0
<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>R' : Type u_1<VAR>A : Type u_2<VAR>Monoid R'<VAR>Semiring A<VAR>(i : ι) → Module A (M₁ i)<VAR>DistribMulAction R' M₂<VAR>Module A M₂<VAR>SMulCommClass A R' M₂<VAR>f : MultilinearMap A M₁ M₂<VAR>c : R'<VAR>m : (i : ι) → M₁ i<GOAL>(c • f) m = c • f m
<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>R' : Type u_1<VAR>A : Type u_2<VAR>Monoid R'<VAR>Semiring A<VAR>(i : ι) → Module A (M₁ i)<VAR>DistribMulAction R' M₂<VAR>Module A M₂<VAR>SMulCommClass A R' M₂<VAR>c : R'<VAR>f : MultilinearMap A M₁ M₂<GOAL>⇑(c • f) = c • ⇑f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<GOAL>∀ (a : MultilinearMap R M₁ M₂) (a_1 : (i : ι) → M₁ i), MultilinearMap.coeAddMonoidHom a a_1 = a a_1
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>α : Type u_1<VAR>f : α → MultilinearMap R M₁ M₂<VAR>s : Finset α<GOAL>⇑(∑ a ∈ s, f a) = ∑ a ∈ s, ⇑(f a)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>α : Type u_1<VAR>f : α → MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<VAR>s : Finset α<GOAL>(∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) 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>AddCommMonoid 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.toLinearMap 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>M₃ : Type v₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>f : MultilinearMap R M₁ M₂<VAR>g : MultilinearMap R M₁ M₃<VAR>m : (i : ι) → M₁ i<GOAL>(f.prod g) m = (f m, g m)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>ι' : Type u_1<VAR>M' : ι' → Type u_2<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → MultilinearMap R M₁ (M' i)<VAR>m : (i : ι) → M₁ i<VAR>i : ι'<GOAL>(MultilinearMap.pi f) m i = (f i) m
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M₂ →ₗ[R] M₃<VAR>x : ι → M₂<GOAL>((MultilinearMap.ofSubsingleton R M₂ M₃ i) f) x = f (x i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>Subsingleton ι<VAR>i : ι<VAR>f : MultilinearMap R (fun x => M₂) M₃<VAR>x : M₂<GOAL>((MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f) x = f fun x_1 => x
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>IsEmpty ι<VAR>m : M₂<GOAL>⇑(MultilinearMap.constOfIsEmpty R M₁ m) = Function.const ((i : ι) → M₁ i) m
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>Semiring 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.succ<VAR>x y : M 0<GOAL>f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>Semiring 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.succ<VAR>c : R<VAR>x : M 0<GOAL>f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>Semiring 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 y : M (Fin.last n)<GOAL>f (Fin.snoc m (x + y)) = f (Fin.snoc m x) + f (Fin.snoc m y)
<VAR>R : Type uR<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₂ : Type v₂<VAR>Semiring 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>c : R<VAR>x : M (Fin.last n)<GOAL>f (Fin.snoc m (c • x)) = c • f (Fin.snoc m x)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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₂<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>m : (i : ι) → M₁ i<GOAL>(g.compLinearMap f) m = g fun i => (f i) (m i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>M₁'' : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (M₁'' i)<VAR>(i : ι) → Module R (M₁'' i)<VAR>g : MultilinearMap R M₁'' M₂<VAR>f₁ : (i : ι) → M₁' i →ₗ[R] M₁'' i<VAR>f₂ : (i : ι) → M₁ i →ₗ[R] M₁' i<GOAL>(g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun i => f₁ i ∘ₗ f₂ i
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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.compLinearMap 0 f = 0
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>AddCommMonoid M₂<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>(g.compLinearMap fun x => LinearMap.id) = g
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>hf : ∀ (i : ι), Function.Surjective ⇑(f i)<GOAL>Function.Injective fun g => g.compLinearMap f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>hf : ∀ (i : ι), Function.Surjective ⇑(f i)<VAR>g₁ g₂ : MultilinearMap R M₁' M₂<GOAL>g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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₂<VAR>f : (i : ι) → M₁ i ≃ₗ[R] M₁' i<GOAL>(g.compLinearMap fun i => ↑(f i)) = 0 ↔ g = 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m m' : (i : ι) → M₁ i<VAR>t : Finset ι<GOAL>f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m m' : (i : ι) → M₁ i<GOAL>f (m + m') = ∑ s : Finset ι, f (s.piecewise m 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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>A : (i : ι) → Finset (α i)<VAR>DecidableEq ι<VAR>Fintype ι<VAR>n : ℕ<VAR>h : ∑ i : ι, (A i).card = n<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>A : (i : ι) → Finset (α i)<VAR>DecidableEq ι<VAR>Fintype ι<GOAL>(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g i (r i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>α : ι → Type u_1<VAR>g : (i : ι) → α i → M₁ i<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → Fintype (α i)<GOAL>(f fun i => ∑ j : α i, g i j) = ∑ r : (i : ι) → α i, f fun i => g i (r i)
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>α : Type u_2<VAR>DecidableEq ι<VAR>t : Finset α<VAR>i : ι<VAR>g : α → M₁ i<VAR>m : (i : ι) → M₁ i<GOAL>f (Function.update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (Function.update m i (g a))
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>p : Submodule R M₂<VAR>h : ∀ (v : (i : ι) → M₁ i), f v ∈ p<VAR>v : (i : ι) → M₁ i<GOAL>↑((f.codRestrict p h) v) = f v
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>A : Type u_1<VAR>Semiring A<VAR>SMul R A<VAR>(i : ι) → Module A (M₁ i)<VAR>Module A M₂<VAR>∀ (i : ι), IsScalarTower R A (M₁ i)<VAR>IsScalarTower R A M₂<VAR>f : MultilinearMap A M₁ M₂<GOAL>⇑(MultilinearMap.restrictScalars R f) = ⇑f
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<VAR>v : ι₂ → M₂<GOAL>(MultilinearMap.domDomCongr σ m) v = m fun i => v (σ i)
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>σ₁ : ι₁ ≃ ι₂<VAR>σ₂ : ι₂ ≃ ι₃<VAR>m : MultilinearMap R (fun x => M₂) M₃<GOAL>MultilinearMap.domDomCongr (σ₁.trans σ₂) m = MultilinearMap.domDomCongr σ₂ (MultilinearMap.domDomCongr σ₁ m)
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>σ₁ σ₂ : Equiv.Perm ι₁<VAR>m : MultilinearMap R (fun x => M₂) M₃<GOAL>MultilinearMap.domDomCongr (σ₂ * σ₁) m = MultilinearMap.domDomCongr σ₂ (MultilinearMap.domDomCongr σ₁ m)
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<GOAL>(MultilinearMap.domDomCongrEquiv σ) m = MultilinearMap.domDomCongr σ m
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<VAR>m : MultilinearMap R (fun x => M₂) M₃<GOAL>(MultilinearMap.domDomCongrEquiv σ).symm m = MultilinearMap.domDomCongr σ.symm m
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<VAR>f g : MultilinearMap R (fun x => M₂) M₃<GOAL>MultilinearMap.domDomCongr σ f = MultilinearMap.domDomCongr σ g ↔ f = g
<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>DecidableEq ι<VAR>P : ι → Prop<VAR>DecidablePred P<VAR>DecidableEq { a // P a }<VAR>x : (i : { a // P a }) → M₁ ↑i<VAR>z : (i : { a // ¬P a }) → M₁ ↑i<VAR>i : { a // P a }<VAR>c : M₁ ↑i<GOAL>(fun j => if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) = Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c
<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>DecidableEq ι<VAR>P : ι → Prop<VAR>DecidablePred P<VAR>DecidableEq { a // ¬P a }<VAR>x : (i : { a // P a }) → M₁ ↑i<VAR>z : (i : { a // ¬P a }) → M₁ ↑i<VAR>i : { a // ¬P a }<VAR>c : M₁ ↑i<GOAL>(fun j => if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) = Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring 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>P : ι → Prop<VAR>DecidablePred P<VAR>x : (i : { a // P a }) → M₁ ↑i<VAR>z : (i : { a // ¬P a }) → M₁ ↑i<GOAL>(f.domDomRestrict P z) x = f fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : MultilinearMap R M₁ M₂<VAR>x y : (i : ι) → M₁ i<GOAL>(f.linearDeriv x) y = ∑ i : ι, f (Function.update x i (y i))
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : MultilinearMap R M₁ M₂<GOAL>⇑(g.compMultilinearMap f) = ⇑g ∘ ⇑f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : MultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<GOAL>(g.compMultilinearMap f) m = g (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>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>p : Submodule R M₂<VAR>h : ∀ (v : (i : ι) → M₁ i), f v ∈ p<GOAL>p.subtype.compMultilinearMap (f.codRestrict p h) = f
<VAR>R : Type uR<VAR>ι : Type uι<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : MultilinearMap R M₁ M₂<VAR>p : Submodule R M₃<VAR>h : ∀ (c : M₂), g c ∈ p<GOAL>(LinearMap.codRestrict p g h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p ⋯
<VAR>R : Type uR<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M'<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M'<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>σ : ι₁ ≃ ι₂<VAR>g : M₂ →ₗ[R] M₃<VAR>f : MultilinearMap R (fun x => M') M₂<GOAL>MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap (MultilinearMap.domDomCongr σ f)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<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 S M₃<VAR>Module R M₃<VAR>SMulCommClass R S M₃<VAR>Subsingleton ι<VAR>i : ι<GOAL>∀ (a : MultilinearMap R (fun x => M₂) M₃), (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i).symm a = (MultilinearMap.ofSubsingleton R M₂ M₃ i).symm a
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<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 S M₃<VAR>Module R M₃<VAR>SMulCommClass R S M₃<VAR>Subsingleton ι<VAR>i : ι<GOAL>∀ (a : M₂ →ₗ[R] M₃), (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i) a = (MultilinearMap.ofSubsingleton R M₂ M₃ i) a
<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 M₁ M₂<GOAL>(MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ) f = { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_add' := ⋯, map_smul' := ⋯ }