ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>v : α →₀ M<VAR>c : R<VAR>h : α → M →ₗ[R] M₂<GOAL>((c • v).sum fun a => ⇑(h a)) = c • v.sum fun a => ⇑(h a)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>α : Type u_4<VAR>Finite α<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<GOAL>∀ (a : α →₀ M) (a_1 : α), (Finsupp.linearEquivFunOnFinite R M α) a a_1 = a a_1
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>α : Type u_4<VAR>Finite α<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>DecidableEq α<VAR>x : α<VAR>m : M<GOAL>(Finsupp.linearEquivFunOnFinite R M α) (Finsupp.single x m) = Pi.single x m
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>α : Type u_4<VAR>Finite α<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>DecidableEq α<VAR>x : α<VAR>m : M<GOAL>(Finsupp.linearEquivFunOnFinite R M α).symm (Pi.single x m) = Finsupp.single x m
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>α : Type u_4<VAR>Finite α<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>f : α →₀ M<GOAL>(Finsupp.linearEquivFunOnFinite R M α).symm ⇑f = f
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>α : Type u_4<VAR>Unique α<VAR>f : α →₀ M<GOAL>(Finsupp.LinearEquiv.finsuppUnique R M α) f = f default
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>α : Type u_4<VAR>Unique α<VAR>m : M<GOAL>(Finsupp.LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>φ ψ : (α →₀ M) →ₗ[R] N<VAR>h : ∀ (a : α) (b : M), φ (Finsupp.single a b) = ψ (Finsupp.single a b)<GOAL>φ = ψ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>φ ψ : (α →₀ M) →ₗ[R] N<VAR>h : ∀ (a : α), φ ∘ₗ Finsupp.lsingle a = ψ ∘ₗ Finsupp.lsingle a<GOAL>φ = ψ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>∀ (a : α →₀ M) (a_1 : α), Finsupp.lcoeFun a a_1 = a a_1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>f : α →₀ M<GOAL>(Finsupp.lsubtypeDomain s) f = Finsupp.subtypeDomain (fun x => x ∈ s) f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : α<VAR>b : M<GOAL>(Finsupp.lsingle a) b = Finsupp.single a b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : α<VAR>f : α →₀ M<GOAL>(Finsupp.lapply a) f = f a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : α<GOAL>Finsupp.lapply a ∘ₗ Finsupp.lsingle a = LinearMap.id
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a a' : α<VAR>h : a ≠ a'<GOAL>Finsupp.lapply a ∘ₗ Finsupp.lsingle a' = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : α<GOAL>LinearMap.ker (Finsupp.lsingle a) = ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>⨆ a ∈ s, LinearMap.range (Finsupp.lsingle a) ≤ ⨅ a ∈ t, LinearMap.ker (Finsupp.lapply a)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⨅ a, LinearMap.ker (Finsupp.lapply a) ≤ ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⨆ a, LinearMap.range (Finsupp.lsingle a) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>Disjoint (⨆ a ∈ s, LinearMap.range (Finsupp.lsingle a)) (⨆ a ∈ t, LinearMap.range (Finsupp.lsingle a))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>a : α<GOAL>Submodule.span R (Finsupp.single a '' s) = Submodule.map (Finsupp.lsingle a) (Submodule.span R s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>p : α →₀ M<GOAL>p ∈ Finsupp.supported M R s ↔ ↑p.support ⊆ s
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>p : α →₀ M<GOAL>p ∈ Finsupp.supported M R s ↔ ∀ x ∉ s, p x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : α →₀ M<GOAL>p ∈ Finsupp.supported M R ↑p.support
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>a : α<VAR>b : M<VAR>h : a ∈ s<GOAL>Finsupp.single a b ∈ Finsupp.supported M R s
<VAR>α : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>s : Set α<GOAL>Finsupp.supported R R s = Submodule.span R ((fun i => Finsupp.single i 1) '' s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>l : α →₀ M<VAR>DecidablePred fun x => x ∈ s<GOAL>↑((Finsupp.restrictDom M R s) l) = Finsupp.filter (fun x => x ∈ s) l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<GOAL>Finsupp.restrictDom M R s ∘ₗ (Finsupp.supported M R s).subtype = LinearMap.id
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<GOAL>LinearMap.range (Finsupp.restrictDom M R s) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<VAR>st : s ⊆ t<GOAL>Finsupp.supported M R s ≤ Finsupp.supported M R t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.supported M R ∅ = ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.supported M R Set.univ = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>δ : Type u_7<VAR>s : δ → Set α<GOAL>Finsupp.supported M R (⋃ i, s i) = ⨆ i, Finsupp.supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<GOAL>Finsupp.supported M R (s ∪ t) = Finsupp.supported M R s ⊔ Finsupp.supported M R t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_7<VAR>s : ι → Set α<GOAL>Finsupp.supported M R (⋂ i, s i) = ⨅ i, Finsupp.supported M R (s i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<GOAL>Finsupp.supported M R (s ∩ t) = Finsupp.supported M R s ⊓ Finsupp.supported M R t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial M<VAR>s t : Set α<GOAL>Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>f : α → M →ₗ[R] N<GOAL>⇑((Finsupp.lsum S) f) = fun d => d.sum fun i => ⇑(f i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>f : α → M →ₗ[R] N<VAR>l : α →₀ M<GOAL>((Finsupp.lsum S) f) l = l.sum fun b => ⇑(f b)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>f : α → M →ₗ[R] N<VAR>i : α<VAR>m : M<GOAL>((Finsupp.lsum S) f) (Finsupp.single i m) = (f i) m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>f : α → M →ₗ[R] N<VAR>i : α<GOAL>(Finsupp.lsum S) f ∘ₗ Finsupp.lsingle i = f i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>f : (α →₀ M) →ₗ[R] N<VAR>x : α<GOAL>(Finsupp.lsum S).symm f x = f ∘ₗ Finsupp.lsingle x
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>X : Type u_7<VAR>f : (X →₀ R) →ₗ[R] M<VAR>x : X<GOAL>(Finsupp.lift M R X).symm f x = f (Finsupp.single x 1)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>X : Type u_7<VAR>f : X → M<VAR>g : X →₀ R<GOAL>((Finsupp.lift M R X) f) g = g.sum fun x r => r • f x
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>X : Type u_7<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : X → M<VAR>x : X →₀ R<GOAL>((Finsupp.llift M R S X) f) x = ((Finsupp.lift M R X) f) x
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>X : Type u_7<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : (X →₀ R) →ₗ[R] M<VAR>x : X<GOAL>(Finsupp.llift M R S X).symm f x = f (Finsupp.single x 1)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>f : α → α'<VAR>l : α →₀ M<GOAL>(Finsupp.lmapDomain M R f) l = Finsupp.mapDomain f l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.lmapDomain M R id = LinearMap.id
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>α'' : Type u_8<VAR>f : α → α'<VAR>g : α' → α''<GOAL>Finsupp.lmapDomain M R (g ∘ f) = Finsupp.lmapDomain M R g ∘ₗ Finsupp.lmapDomain M R f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>f : α → α'<VAR>s : Set α'<GOAL>Finsupp.supported M R (f ⁻¹' s) ≤ Submodule.comap (Finsupp.lmapDomain M R f) (Finsupp.supported M R s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>f : α → α'<VAR>s : Set α<GOAL>Submodule.map (Finsupp.lmapDomain M R f) (Finsupp.supported M R s) = Finsupp.supported M R (f '' s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>f : α → α'<VAR>s : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b<GOAL>Disjoint (Finsupp.supported M R s) (LinearMap.ker (Finsupp.lmapDomain M R f))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>l : α →₀ R<GOAL>(Finsupp.total α M R v) l = l.sum fun i a => a • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>l : α →₀ R<VAR>s : Finset α<VAR>hs : l ∈ Finsupp.supported R R ↑s<GOAL>(Finsupp.total α M R v) l = ∑ i ∈ s, l i • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>c : R<VAR>a : α<GOAL>(Finsupp.total α M R v) (Finsupp.single a c) = c • v a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : α →₀ R<GOAL>(Finsupp.total α M R 0) x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.total α M R 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>v : α → M<VAR>l : α →₀ R<GOAL>f ((Finsupp.total α M R v) l) = (Finsupp.total α M' R (⇑f ∘ v)) l
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>l : M →₀ R<GOAL>f ((Finsupp.total M M R id) l) = (Finsupp.total M M' R ⇑f) l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Unique α<VAR>l : α →₀ R<VAR>v : α → M<GOAL>(Finsupp.total α M R v) l = l default • v default
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>h : Function.Surjective v<GOAL>Function.Surjective ⇑(Finsupp.total α M R v)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>h : Function.Surjective v<GOAL>LinearMap.range (Finsupp.total α M R v) = ⊤
<VAR>R : Type u_5<VAR>Semiring R<VAR>M : Type u_9<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.Surjective ⇑(Finsupp.total M M R id)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<GOAL>LinearMap.range (Finsupp.total α M R v) = Submodule.span R (Set.range v)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α → α'<VAR>g : M →ₗ[R] M'<VAR>h : ∀ (i : α), g (v i) = v' (f i)<GOAL>Finsupp.total α' M' R v' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.total α M R v
<VAR>α : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>v' : α' → M'<VAR>f : α → α'<GOAL>Finsupp.total α' M' R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.total α M' R (v' ∘ f)
<VAR>α : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>v' : α' → M'<VAR>f : α ↪ α'<VAR>l : α →₀ R<GOAL>(Finsupp.total α' M' R v') (Finsupp.embDomain f l) = (Finsupp.total α M' R (v' ∘ ⇑f)) l
<VAR>α : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>v' : α' → M'<VAR>f : α → α'<VAR>l : α →₀ R<GOAL>(Finsupp.total α' M' R v') (Finsupp.mapDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l
<VAR>α : Type u_1<VAR>R : Type u_5<VAR>Semiring R<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>v' : α' → M'<VAR>f : α ≃ α'<VAR>l : α →₀ R<GOAL>(Finsupp.total α' M' R v') (Finsupp.equivMapDomain f l) = (Finsupp.total α M' R (v' ∘ ⇑f)) l
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R s = LinearMap.range (Finsupp.total (↑s) M R Subtype.val)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ Submodule.span R s ↔ ∃ l, (Finsupp.total (↑s) M R Subtype.val) l = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>x : M<GOAL>x ∈ Submodule.span R (Set.range v) ↔ ∃ c, (c.sum fun i a => a • v i) = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>s : Set α<GOAL>Submodule.span R (v '' s) = Submodule.map (Finsupp.total α M R v) (Finsupp.supported R R s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>s : Set α<VAR>x : M<GOAL>x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ Finsupp.supported R R s, (Finsupp.total α M R v) l = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : Option α → M<VAR>f : Option α →₀ R<GOAL>(Finsupp.total (Option α) M R v) f = f none • v none + (Finsupp.total α M R (v ∘ some)) f.some
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_9<VAR>β : Type u_10<VAR>A : α → M<VAR>B : β → α →₀ R<VAR>f : β →₀ R<GOAL>(Finsupp.total α M R A) ((Finsupp.total β (α →₀ R) R B) f) = (Finsupp.total β M R fun b => (Finsupp.total α M R A) (B b)) f
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Fin 0 → M<GOAL>Finsupp.total (Fin 0) M R f = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : α → M<VAR>s : Set α<GOAL>LinearMap.range (Finsupp.totalOn α M R v s) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>v : α → M<VAR>f : α' → α<GOAL>Finsupp.total α' M R (v ∘ f) = Finsupp.total α M R v ∘ₗ Finsupp.lmapDomain R R f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α' : Type u_7<VAR>v : α → M<VAR>f : α → α'<VAR>l : α' →₀ R<VAR>hf : Set.InjOn f (f ⁻¹' ↑l.support)<GOAL>(Finsupp.total α M R v) (Finsupp.comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Finset α<VAR>f : α → R<VAR>g : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<GOAL>(Finsupp.total α M R g) (Finsupp.onFinset s f hf) = ∑ x ∈ s, f x • g x
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α₁ : Type u_7<VAR>α₂ : Type u_8<VAR>e : α₁ ≃ α₂<VAR>v : α₁ →₀ M<GOAL>(Finsupp.domLCongr e) v = (Finsupp.domCongr e) v
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α₁ : Type u_7<VAR>α₂ : Type u_8<VAR>α₃ : Type u_9<VAR>f : α₁ ≃ α₂<VAR>f₂ : α₂ ≃ α₃<GOAL>Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂ = Finsupp.domLCongr (f.trans f₂)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α₁ : Type u_7<VAR>α₂ : Type u_8<VAR>f : α₁ ≃ α₂<GOAL>(Finsupp.domLCongr f).symm = Finsupp.domLCongr f.symm
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α₁ : Type u_7<VAR>α₂ : Type u_8<VAR>e : α₁ ≃ α₂<VAR>i : α₁<VAR>m : M<GOAL>(Finsupp.domLCongr e) (Finsupp.single i m) = Finsupp.single (e i) m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.linearMap f) g = Finsupp.mapRange ⇑f ⋯ g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.mapRange.linearMap LinearMap.id = LinearMap.id
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>f₂ : M →ₗ[R] N<GOAL>Finsupp.mapRange.linearMap (f ∘ₗ f₂) = Finsupp.mapRange.linearMap f ∘ₗ Finsupp.mapRange.linearMap f₂
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>(Finsupp.mapRange.linearMap f).toAddMonoidHom = Finsupp.mapRange.addMonoidHom f.toAddMonoidHom
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<VAR>g : α →₀ M<GOAL>(Finsupp.mapRange.linearEquiv e) g = (Finsupp.mapRange.linearMap ↑e) g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Finsupp.mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>f : M ≃ₗ[R] N<VAR>f₂ : N ≃ₗ[R] P<GOAL>Finsupp.mapRange.linearEquiv (f ≪≫ₗ f₂) = Finsupp.mapRange.linearEquiv f ≪≫ₗ Finsupp.mapRange.linearEquiv f₂
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M ≃ₗ[R] N<GOAL>(Finsupp.mapRange.linearEquiv f).symm = Finsupp.mapRange.linearEquiv f.symm
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M ≃ₗ[R] N<GOAL>(Finsupp.mapRange.linearEquiv f).toAddEquiv = Finsupp.mapRange.addEquiv f.toAddEquiv
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M ≃ₗ[R] N<GOAL>↑(Finsupp.mapRange.linearEquiv f) = Finsupp.mapRange.linearMap ↑f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>e₁ : ι ≃ κ<VAR>e₂ : M ≃ₗ[R] N<VAR>i : ι<VAR>m : M<GOAL>(Finsupp.lcongr e₁ e₂) (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>e₁ : ι ≃ κ<VAR>e₂ : M ≃ₗ[R] N<VAR>f : ι →₀ M<VAR>k : κ<GOAL>((Finsupp.lcongr e₁ e₂) f) k = e₂ (f (e₁.symm k))
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>e₁ : ι ≃ κ<VAR>e₂ : M ≃ₗ[R] N<VAR>k : κ<VAR>n : N<GOAL>(Finsupp.lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>e₁ : ι ≃ κ<VAR>e₂ : M ≃ₗ[R] N<GOAL>(Finsupp.lcongr e₁ e₂).symm = Finsupp.lcongr e₁.symm e₂.symm
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<GOAL>∀ (a : (α →₀ M) × (β →₀ M)), (Finsupp.sumFinsuppLEquivProdFinsupp R).symm a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<GOAL>∀ (a : α ⊕ β →₀ M), (Finsupp.sumFinsuppLEquivProdFinsupp R) a = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<VAR>f : α ⊕ β →₀ M<VAR>x : α<GOAL>((Finsupp.sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<VAR>f : α ⊕ β →₀ M<VAR>y : β<GOAL>((Finsupp.sumFinsuppLEquivProdFinsupp R) f).2 y = f (Sum.inr y)
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<VAR>fg : (α →₀ M) × (β →₀ M)<VAR>x : α<GOAL>((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x
<VAR>M : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>β : Type u_8<VAR>fg : (α →₀ M) × (β →₀ M)<VAR>y : β<GOAL>((Finsupp.sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y
<VAR>R : Type u_5<VAR>Semiring R<VAR>η : Type u_7<VAR>Fintype η<VAR>M : Type u_9<VAR>ιs : η → Type u_10<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : (j : η) × ιs j →₀ M<VAR>j : η<VAR>i : ιs j<GOAL>((Finsupp.sigmaFinsuppLEquivPiFinsupp R) f j) i = f ⟨j, i⟩