ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N O : Submodule R M<VAR>y : M<VAR>yO : y ∈ O<VAR>b : Basis (Fin n) R ↥N<VAR>hNO : N ≤ O<VAR>hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0<VAR>hsp : ∀ z ∈ O, ∃ c, z + c • y ∈ N<GOAL>⇑(Basis.mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons ⟨y, yO⟩ (⇑(Submodule.inclusion hNO) ∘ ⇑b)
<VAR>R : Type u_10<VAR>Semiring R<GOAL>(Basis.finTwoProd R) 0 = (1, 0)
<VAR>R : Type u_10<VAR>Semiring R<GOAL>(Basis.finTwoProd R) 1 = (0, 1)
<VAR>R : Type u_10<VAR>Semiring R<VAR>x : R × R<GOAL>⇑((Basis.finTwoProd R).repr x) = ![x.1, x.2]
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_10<VAR>Semiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>SMulCommClass R R A<VAR>IsScalarTower R A A<VAR>b : Basis ι R A<VAR>z : A<GOAL>z ∈ Set.center A ↔ (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>S : Type u_10<VAR>CommRing R<VAR>Ring S<VAR>Nontrivial S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>i : ι<GOAL>↑((Basis.restrictScalars R b) i) = b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>S : Type u_10<VAR>CommRing R<VAR>Ring S<VAR>Nontrivial S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : ↥(Submodule.span R (Set.range ⇑b))<VAR>i : ι<GOAL>(algebraMap R S) (((Basis.restrictScalars R b).repr m) i) = (b.repr ↑m) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>S : Type u_10<VAR>CommRing R<VAR>Ring S<VAR>Nontrivial S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : M<GOAL>m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Nontrivial R<VAR>Module R M<VAR>w : Set M<VAR>hw : w.Finite<VAR>s : Submodule.span R w = ⊤<VAR>ι : Type w<VAR>b : Basis ι R M<GOAL>Finite ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Nontrivial R<VAR>Module R M<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>⋃ k, ↑(b.repr (v k)).support = Set.univ
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Nontrivial R<VAR>Module R M<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>Infinite ι<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Nontrivial R<VAR>Module R M<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>Cardinal.mk ι ≤ Cardinal.mk κ
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>self : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>i j : ι<GOAL>v i = v j → i ≠ j → (↑self).toFun v = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>(↑f).toFun = ⇑f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : MultilinearMap R (fun x => M) N<VAR>h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0<GOAL>⇑{ toMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f g : M [⋀^ι]→ₗ[R] N<VAR>h : f = g<VAR>x : ι → M<GOAL>f x = g x
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>x y : ι → M<VAR>h : x = y<GOAL>f x = f y
<VAR>R : Type u_1<VAR>Semiring 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_7<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f g : M [⋀^ι]→ₗ[R] N<GOAL>⇑f = ⇑g ↔ f = g
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>H : ∀ (x : ι → M), f x = f' x<GOAL>f = f'
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f g : M [⋀^ι]→ₗ[R] N<GOAL>f = g ↔ ∀ (x : ι → M), f x = g x
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>Semiring 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_7<GOAL>Function.Injective AlternatingMap.toMultilinearMap
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : (ι → M) → N<VAR>h₁ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)<VAR>h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (Function.update m i (c • x)) = c • f (Function.update m i x)<VAR>h₃ : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → { toFun := f, map_add' := ⋯, map_smul' := ⋯ }.toFun v = 0<GOAL>↑{ toFun := f, map_add' := ⋯, map_smul' := ⋯, map_eq_zero_of_eq' := h₃ } = { toFun := f, map_add' := h₁, map_smul' := h₂ }
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i : ι<VAR>x y : M<GOAL>f (Function.update v i (x + y)) = f (Function.update v i x) + f (Function.update v i y)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M' : Type u_5<VAR>AddCommGroup M'<VAR>Module R M'<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v' : ι → M'<VAR>DecidableEq ι<VAR>i : ι<VAR>x y : M'<GOAL>g' (Function.update v' i (x - y)) = g' (Function.update v' i x) - g' (Function.update v' i y)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M' : Type u_5<VAR>AddCommGroup M'<VAR>Module R M'<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v' : ι → M'<VAR>DecidableEq ι<VAR>i : ι<VAR>x : M'<GOAL>g' (Function.update v' i (-x)) = -g' (Function.update v' i x)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i : ι<VAR>r : R<VAR>x : M<GOAL>f (Function.update v i (r • x)) = r • f (Function.update v i x)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>i j : ι<VAR>h : v i = v j<VAR>hij : i ≠ j<GOAL>f v = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>m : ι → M<VAR>i : ι<VAR>h : m i = 0<GOAL>f m = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<GOAL>f (Function.update m i 0) = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>Nonempty ι<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>hv : ¬Function.Injective v<GOAL>f v = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>S : Type u_10<VAR>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass R S N<VAR>c : S<VAR>m : ι → M<GOAL>(c • f) m = c • f m
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>S : Type u_10<VAR>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass R S N<VAR>c : S<GOAL>↑(c • f) = c • ↑f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>S : Type u_10<VAR>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass R S N<VAR>c : S<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>⇑(c • f) = c • ⇑f
<VAR>R : Type u_1<VAR>Semiring 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>P : Type u_4<VAR>AddCommMonoid P<VAR>Module R P<VAR>ι : Type u_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g : M [⋀^ι]→ₗ[R] P<VAR>m : (i : ι) → (fun x => M) i<GOAL>(f.prod g) m = (f m, g m)
<VAR>R : Type u_1<VAR>Semiring 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>P : Type u_4<VAR>AddCommMonoid P<VAR>Module R P<VAR>ι : Type u_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g : M [⋀^ι]→ₗ[R] P<GOAL>↑(f.prod g) = (↑f).prod ↑g
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_7<VAR>ι' : Type u_10<VAR>N : ι' → Type u_11<VAR>(i : ι') → AddCommMonoid (N i)<VAR>(i : ι') → Module R (N i)<VAR>f : (i : ι') → M [⋀^ι]→ₗ[R] N i<VAR>m : (i : ι) → (fun x => M) i<VAR>i : ι'<GOAL>(AlternatingMap.pi f) m i = (f i) m
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_7<VAR>ι' : Type u_10<VAR>N : ι' → Type u_11<VAR>(i : ι') → AddCommMonoid (N i)<VAR>(i : ι') → Module R (N i)<VAR>f : (i : ι') → M [⋀^ι]→ₗ[R] N i<GOAL>↑(AlternatingMap.pi f) = MultilinearMap.pi fun a => ↑(f a)
<VAR>R : Type u_10<VAR>M₁ : Type u_11<VAR>M₂ : Type u_12<VAR>ι : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>f : M₁ [⋀^ι]→ₗ[R] R<VAR>z : M₂<GOAL>∀ (a : (i : ι) → (fun x => M₁) i), (f.smulRight z) a = f a • z
<VAR>R : Type u_10<VAR>M₁ : Type u_11<VAR>M₂ : Type u_12<VAR>ι : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>f : M₁ [⋀^ι]→ₗ[R] R<VAR>z : M₂<GOAL>↑(f.smulRight z) = (↑f).smulRight z
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<GOAL>(f + f') v = f v + f' v
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f f' : M [⋀^ι]→ₗ[R] N<GOAL>↑(f + f') = ↑f + ↑f'
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>v : ι → M<GOAL>0 v = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<GOAL>{ toMultilinearMap := 0, map_eq_zero_of_eq' := ⋯ } = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<VAR>m : ι → M<GOAL>(-g) m = -g m
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<GOAL>↑(-g) = -↑g
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>m : ι → M<GOAL>(g - g₂) m = g m - g₂ m
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<GOAL>↑(g - g₂) = ↑g - ↑g₂
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M →ₗ[R] N<VAR>x : ι → M<GOAL>((AlternatingMap.ofSubsingleton R M N i) f) x = f (x i)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>x : M<GOAL>((AlternatingMap.ofSubsingleton R M N i).symm f) x = f fun x_1 => x
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>IsEmpty ι<VAR>m : N<GOAL>⇑(AlternatingMap.constOfIsEmpty R M ι m) = Function.const (ι → M) m
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>p : Submodule R N<VAR>h : ∀ (v : ι → M), f v ∈ p<VAR>v : ι → M<GOAL>↑((f.codRestrict p h) v) = f v
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>N₂ : Type u_10<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>g : N →ₗ[R] N₂<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>⇑(g.compAlternatingMap f) = ⇑g ∘ ⇑f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>N₂ : Type u_10<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>g : N →ₗ[R] N₂<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>m : ι → M<GOAL>(g.compAlternatingMap f) m = g (f m)
<VAR>R : Type u_11<VAR>M₁ : Type u_12<VAR>M₂ : Type u_13<VAR>ι : Type u_14<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>f : M₁ [⋀^ι]→ₗ[R] R<VAR>z : M₂<GOAL>f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>p : Submodule R N<VAR>h : ∀ (v : ι → M), f v ∈ p<GOAL>p.subtype.compAlternatingMap (f.codRestrict p h) = f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>N₂ : Type u_10<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>g : N →ₗ[R] N₂<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>p : Submodule R N₂<VAR>h : ∀ (c : N), g c ∈ p<GOAL>(LinearMap.codRestrict p g h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p ⋯
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g : M₂ →ₗ[R] M<GOAL>⇑(f.compLinearMap g) = ⇑f ∘ fun x => ⇑g ∘ x
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g : M₂ →ₗ[R] M<VAR>v : ι → M₂<GOAL>(f.compLinearMap g) v = f fun i => g (v i)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>M₃ : Type u_11<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g₁ : M₂ →ₗ[R] M<VAR>g₂ : M₃ →ₗ[R] M₂<GOAL>(f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>g : M₂ →ₗ[R] M<GOAL>AlternatingMap.compLinearMap 0 g = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f₁ f₂ : M [⋀^ι]→ₗ[R] N<VAR>g : M₂ →ₗ[R] M<GOAL>(f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Nonempty ι<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>f.compLinearMap 0 = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>f.compLinearMap LinearMap.id = f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₂ →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective fun g => g.compLinearMap f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₂ →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>g₁ g₂ : M [⋀^ι]→ₗ[R] N<GOAL>g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>e : M ≃ₗ[R] M₂<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>(AlternatingMap.domLCongr R N ι S e) f = f.compLinearMap ↑e.symm
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<GOAL>AlternatingMap.domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>e : M ≃ₗ[R] M₂<GOAL>(AlternatingMap.domLCongr R N ι S e).symm = AlternatingMap.domLCongr R N ι S e.symm
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>M₃ : Type u_11<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>e : M ≃ₗ[R] M₂<VAR>f : M₂ ≃ₗ[R] M₃<GOAL>AlternatingMap.domLCongr R N ι S e ≪≫ₗ AlternatingMap.domLCongr R N ι S f = AlternatingMap.domLCongr R N ι S (e ≪≫ₗ f)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>M₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>g : M₂ ≃ₗ[R] M<GOAL>f.compLinearMap ↑g = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>α : Type u_12<VAR>DecidableEq ι<VAR>t : Finset α<VAR>i : ι<VAR>g : α → M<VAR>m : ι → M<GOAL>f (Function.update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (Function.update m i (g a))
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f (Function.update v i (v j)) = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>m : M<GOAL>f (Function.update (Function.update v i m) j m) = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f (v ∘ ⇑(Equiv.swap i j)) + f v = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f v + f (v ∘ ⇑(Equiv.swap i j)) = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>g (v ∘ ⇑(Equiv.swap i j)) = -g v
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<VAR>DecidableEq ι<VAR>Fintype ι<VAR>v : ι → M<VAR>σ : Equiv.Perm ι<GOAL>g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>DecidableEq ι<VAR>Fintype ι<VAR>σ : Equiv.Perm ι<GOAL>g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>v : ι' → M<GOAL>(AlternatingMap.domDomCongr σ f) v = f (v ∘ ⇑σ)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr (Equiv.refl ι) f = f
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>σ₁ : ι ≃ ι'<VAR>σ₂ : ι' ≃ ι''<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr (σ₁.trans σ₂) f = AlternatingMap.domDomCongr σ₂ (AlternatingMap.domDomCongr σ₁ f)
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<GOAL>AlternatingMap.domDomCongr σ 0 = 0
<VAR>R : Type u_1<VAR>Semiring 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_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f g : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr σ (f + g) = AlternatingMap.domDomCongr σ f + AlternatingMap.domDomCongr σ g