Documentation

Mathlib.LinearAlgebra.Finsupp

Properties of the module α →₀ M #

Given an R-module M, the R-module structure on α →₀ M is defined in Data.Finsupp.Basic.

In this file we define Finsupp.supported s to be the set {f : α →₀ M | f.support ⊆ s} interpreted as a submodule of α →₀ M. We also define LinearMap versions of various maps:

Tags #

function with finite support, module, linear algebra

theorem Finsupp.smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [Zero β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : αβM} :
c Finsupp.sum v h = Finsupp.sum v fun (a : α) (b : β) => c h a b
@[simp]
theorem Finsupp.sum_smul_index_linearMap' {α : Type u_1} {R : Type u_3} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R} {h : αM →ₗ[R] M₂} :
(Finsupp.sum (c v) fun (a : α) => (h a)) = c Finsupp.sum v fun (a : α) => (h a)
@[simp]
theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] :
∀ (a : α →₀ M) (a_1 : α), (Finsupp.linearEquivFunOnFinite R M α) a a_1 = a a_1
noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] :
(α →₀ M) ≃ₗ[R] αM

Given Finite α, linearEquivFunOnFinite R is the natural R-linear equivalence between α →₀ β and α → β.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) :
    @[simp]
    theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) :
    @[simp]
    theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (f : α →₀ M) :
    noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_3) [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] :
    (α →₀ M) ≃ₗ[R] M

    If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] (f : α →₀ M) :
      @[simp]
      def Finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) :

      Interpret Finsupp.single a as a linear map.

      Equations
      Instances For
        theorem Finsupp.lhom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] ⦃φ : (α →₀ M) →ₗ[R] N ⦃ψ : (α →₀ M) →ₗ[R] N (h : ∀ (a : α) (b : M), φ (Finsupp.single a b) = ψ (Finsupp.single a b)) :
        φ = ψ

        Two R-linear maps from Finsupp X M which agree on each single x y agree everywhere.

        theorem Finsupp.lhom_ext' {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] ⦃φ : (α →₀ M) →ₗ[R] N ⦃ψ : (α →₀ M) →ₗ[R] N (h : ∀ (a : α), φ ∘ₗ Finsupp.lsingle a = ψ ∘ₗ Finsupp.lsingle a) :
        φ = ψ

        Two R-linear maps from Finsupp X M which agree on each single x y agree everywhere.

        We formulate this fact using equality of linear maps φ.comp (lsingle a) and ψ.comp (lsingle a) so that the ext tactic can apply a type-specific extensionality lemma to prove equality of these maps. E.g., if M = R, then it suffices to verify φ (single a 1) = ψ (single a 1).

        def Finsupp.lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) :
        (α →₀ M) →ₗ[R] M

        Interpret fun f : α →₀ M ↦ f a as a linear map.

        Equations
        Instances For
          instance LinearMap.CompatibleSMul.finsupp_dom (R : Type u_7) (S : Type u_8) (M : Type u_9) (N : Type u_10) (ι : Type u_11) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMulZeroClass R M] [DistribSMul R N] [LinearMap.CompatibleSMul M N R S] :
          Equations
          • =
          instance LinearMap.CompatibleSMul.finsupp_cod (R : Type u_7) (S : Type u_8) (M : Type u_9) (N : Type u_10) (ι : Type u_11) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMul R M] [SMulZeroClass R N] [LinearMap.CompatibleSMul M N R S] :
          Equations
          • =
          @[simp]
          theorem Finsupp.lcoeFun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
          ∀ (a : α →₀ M) (a_1 : α), Finsupp.lcoeFun a a_1 = a a_1
          def Finsupp.lcoeFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
          (α →₀ M) →ₗ[R] αM

          Forget that a function is finitely supported.

          This is the linear version of Finsupp.toFun.

          Equations
          • Finsupp.lcoeFun = { toAddHom := { toFun := DFunLike.coe, map_add' := }, map_smul' := }
          Instances For
            def Finsupp.lsubtypeDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) :
            (α →₀ M) →ₗ[R] s →₀ M

            Interpret Finsupp.subtypeDomain s as a linear map.

            Equations
            Instances For
              theorem Finsupp.lsubtypeDomain_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (f : α →₀ M) :
              (Finsupp.lsubtypeDomain s) f = Finsupp.subtypeDomain (fun (x : α) => x s) f
              @[simp]
              theorem Finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (b : M) :
              @[simp]
              theorem Finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (f : α →₀ M) :
              (Finsupp.lapply a) f = f a
              @[simp]
              theorem Finsupp.lapply_comp_lsingle_same {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) :
              Finsupp.lapply a ∘ₗ Finsupp.lsingle a = LinearMap.id
              @[simp]
              theorem Finsupp.lapply_comp_lsingle_of_ne {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (a' : α) (h : a a') :
              @[simp]
              theorem Finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) :
              theorem Finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) (h : Disjoint s t) :
              theorem Finsupp.iInf_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
              theorem Finsupp.iSup_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
              theorem Finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) (hs : Disjoint s t) :
              theorem Finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (a : α) :
              def Finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) :
              Submodule R (α →₀ M)

              Finsupp.supported M R s is the R-submodule of all p : α →₀ M such that p.support ⊆ s.

              Equations
              • Finsupp.supported M R s = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {p : α →₀ M | p.support s}, add_mem' := }, zero_mem' := }, smul_mem' := }
              Instances For
                theorem Finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) :
                p Finsupp.supported M R s p.support s
                theorem Finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) :
                p Finsupp.supported M R s xs, p x = 0
                theorem Finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (p : α →₀ M) :
                p Finsupp.supported M R p.support
                theorem Finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {a : α} (b : M) (h : a s) :
                theorem Finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_5) [Semiring R] (s : Set α) :
                Finsupp.supported R R s = Submodule.span R ((fun (i : α) => Finsupp.single i 1) '' s)
                def Finsupp.restrictDom {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
                (α →₀ M) →ₗ[R] (Finsupp.supported M R s)

                Interpret Finsupp.filter s as a linear map from α →₀ M to supported M R s.

                Equations
                Instances For
                  @[simp]
                  theorem Finsupp.restrictDom_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (l : α →₀ M) [DecidablePred fun (x : α) => x s] :
                  ((Finsupp.restrictDom M R s) l) = Finsupp.filter (fun (x : α) => x s) l
                  theorem Finsupp.restrictDom_comp_subtype {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
                  Finsupp.restrictDom M R s ∘ₗ Submodule.subtype (Finsupp.supported M R s) = LinearMap.id
                  theorem Finsupp.range_restrictDom {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
                  theorem Finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {t : Set α} (st : s t) :
                  @[simp]
                  theorem Finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
                  @[simp]
                  theorem Finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
                  Finsupp.supported M R Set.univ =
                  theorem Finsupp.supported_iUnion {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {δ : Type u_7} (s : δSet α) :
                  Finsupp.supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), Finsupp.supported M R (s i)
                  theorem Finsupp.supported_union {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) :
                  theorem Finsupp.supported_iInter {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} (s : ιSet α) :
                  Finsupp.supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), Finsupp.supported M R (s i)
                  theorem Finsupp.supported_inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) :
                  theorem Finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {t : Set α} (h : Disjoint s t) :
                  theorem Finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s : Set α} {t : Set α} :
                  def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) :
                  (Finsupp.supported M R s) ≃ₗ[R] s →₀ M

                  Interpret Finsupp.restrictSupportEquiv as a linear equivalence between supported M R s and s →₀ M.

                  Equations
                  Instances For
                    def Finsupp.lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] :
                    (αM →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N

                    Lift a family of linear maps M →ₗ[R] N indexed by x : α to a linear map from α →₀ M to N using Finsupp.sum. This is an upgraded version of Finsupp.liftAddHom.

                    See note [bundled maps over different rings] for why separate R and S semirings are used.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Finsupp.coe_lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : αM →ₗ[R] N) :
                      ((Finsupp.lsum S) f) = fun (d : α →₀ M) => Finsupp.sum d fun (i : α) => (f i)
                      theorem Finsupp.lsum_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : αM →ₗ[R] N) (l : α →₀ M) :
                      ((Finsupp.lsum S) f) l = Finsupp.sum l fun (b : α) => (f b)
                      theorem Finsupp.lsum_single {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : αM →ₗ[R] N) (i : α) (m : M) :
                      ((Finsupp.lsum S) f) (Finsupp.single i m) = (f i) m
                      @[simp]
                      theorem Finsupp.lsum_comp_lsingle {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : αM →ₗ[R] N) (i : α) :
                      (Finsupp.lsum S) f ∘ₗ Finsupp.lsingle i = f i
                      theorem Finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : (α →₀ M) →ₗ[R] N) (x : α) :
                      noncomputable def Finsupp.lift (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) :
                      (XM) ≃+ ((X →₀ R) →ₗ[R] M)

                      A slight rearrangement from lsum gives us the bijection underlying the free-forgetful adjunction for R-modules.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Finsupp.lift_symm_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) (f : (X →₀ R) →ₗ[R] M) (x : X) :
                        @[simp]
                        theorem Finsupp.lift_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) (f : XM) (g : X →₀ R) :
                        ((Finsupp.lift M R X) f) g = Finsupp.sum g fun (x : X) (r : R) => r f x
                        noncomputable def Finsupp.llift (M : Type u_2) (R : Type u_5) (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass R S M] :
                        (XM) ≃ₗ[S] (X →₀ R) →ₗ[R] M

                        Given compatible S and R-module structures on M and a type X, the set of functions X → M is S-linearly equivalent to the R-linear maps from the free R-module on X to M.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem Finsupp.llift_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass R S M] (f : XM) (x : X →₀ R) :
                          ((Finsupp.llift M R S X) f) x = ((Finsupp.lift M R X) f) x
                          @[simp]
                          theorem Finsupp.llift_symm_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass R S M] (f : (X →₀ R) →ₗ[R] M) (x : X) :
                          def Finsupp.lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : αα') :
                          (α →₀ M) →ₗ[R] α' →₀ M

                          Interpret Finsupp.mapDomain as a linear map.

                          Equations
                          Instances For
                            @[simp]
                            theorem Finsupp.lmapDomain_apply {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : αα') (l : α →₀ M) :
                            @[simp]
                            theorem Finsupp.lmapDomain_id {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :
                            Finsupp.lmapDomain M R id = LinearMap.id
                            theorem Finsupp.lmapDomain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {α'' : Type u_8} (f : αα') (g : α'α'') :
                            theorem Finsupp.supported_comap_lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : αα') (s : Set α') :
                            theorem Finsupp.lmapDomain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : αα') (s : Set α) :
                            theorem Finsupp.lmapDomain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : αα') {s : Set α} (H : as, bs, f a = f ba = b) :
                            def Finsupp.lcomapDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {β : Type u_7} (f : αβ) (hf : Function.Injective f) :
                            (β →₀ M) →ₗ[R] α →₀ M

                            Given f : α → β and a proof hf that f is injective, lcomapDomain f hf is the linear map sending l : β →₀ M to the finitely supported function from α to M given by composing l with f.

                            This is the linear version of Finsupp.comapDomain.

                            Equations
                            Instances For
                              def Finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : αM) :
                              (α →₀ R) →ₗ[R] M

                              Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

                              Equations
                              Instances For
                                theorem Finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (l : α →₀ R) :
                                (Finsupp.total α M R v) l = Finsupp.sum l fun (i : α) (a : R) => a v i
                                theorem Finsupp.total_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} {l : α →₀ R} {s : Finset α} (hs : l Finsupp.supported R R s) :
                                (Finsupp.total α M R v) l = Finset.sum s fun (i : α) => l i v i
                                @[simp]
                                theorem Finsupp.total_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (c : R) (a : α) :
                                (Finsupp.total α M R v) (Finsupp.single a c) = c v a
                                theorem Finsupp.total_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : α →₀ R) :
                                (Finsupp.total α M R 0) x = 0
                                @[simp]
                                theorem Finsupp.total_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :
                                Finsupp.total α M R 0 = 0
                                theorem Finsupp.apply_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (v : αM) (l : α →₀ R) :
                                f ((Finsupp.total α M R v) l) = (Finsupp.total α M' R (f v)) l
                                theorem Finsupp.apply_total_id {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (l : M →₀ R) :
                                f ((Finsupp.total M M R id) l) = (Finsupp.total M M' R f) l
                                theorem Finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Unique α] (l : α →₀ R) (v : αM) :
                                (Finsupp.total α M R v) l = l default v default
                                theorem Finsupp.total_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (h : Function.Surjective v) :
                                theorem Finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (h : Function.Surjective v) :
                                theorem Finsupp.total_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] :

                                Any module is a quotient of a free module. This is stated as surjectivity of Finsupp.total M M R id : (M →₀ R) →ₗ[R] M.

                                theorem Finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} :
                                theorem Finsupp.lmapDomain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : αM} {v' : α'M'} (f : αα') (g : M →ₗ[R] M') (h : ∀ (i : α), g (v i) = v' (f i)) :
                                Finsupp.total α' M' R v' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.total α M R v
                                theorem Finsupp.total_comp_lmapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α'M'} (f : αα') :
                                Finsupp.total α' M' R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.total α M' R (v' f)
                                @[simp]
                                theorem Finsupp.total_embDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α'M'} (f : α α') (l : α →₀ R) :
                                (Finsupp.total α' M' R v') (Finsupp.embDomain f l) = (Finsupp.total α M' R (v' f)) l
                                @[simp]
                                theorem Finsupp.total_mapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α'M'} (f : αα') (l : α →₀ R) :
                                (Finsupp.total α' M' R v') (Finsupp.mapDomain f l) = (Finsupp.total α M' R (v' f)) l
                                @[simp]
                                theorem Finsupp.total_equivMapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α'M'} (f : α α') (l : α →₀ R) :
                                (Finsupp.total α' M' R v') (Finsupp.equivMapDomain f l) = (Finsupp.total α M' R (v' f)) l
                                theorem Finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
                                Submodule.span R s = LinearMap.range (Finsupp.total (s) M R Subtype.val)

                                A version of Finsupp.range_total which is useful for going in the other direction

                                theorem Finsupp.mem_span_iff_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (x : M) :
                                x Submodule.span R s ∃ (l : s →₀ R), (Finsupp.total (s) M R Subtype.val) l = x
                                theorem Finsupp.mem_span_range_iff_exists_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} {x : M} :
                                x Submodule.span R (Set.range v) ∃ (c : α →₀ R), (Finsupp.sum c fun (i : α) (a : R) => a v i) = x
                                theorem Finsupp.span_image_eq_map_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (s : Set α) :
                                theorem Finsupp.mem_span_image_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} {s : Set α} {x : M} :
                                x Submodule.span R (v '' s) ∃ l ∈ Finsupp.supported R R s, (Finsupp.total α M R v) l = x
                                theorem Finsupp.total_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : Option αM) (f : Option α →₀ R) :
                                (Finsupp.total (Option α) M R v) f = f none v none + (Finsupp.total α M R (v some)) (Finsupp.some f)
                                theorem Finsupp.total_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} {β : Type u_10} (A : αM) (B : βα →₀ R) (f : β →₀ R) :
                                (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
                                @[simp]
                                theorem Finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0M) :
                                Finsupp.total (Fin 0) M R f = 0
                                def Finsupp.totalOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : αM) (s : Set α) :
                                (Finsupp.supported R R s) →ₗ[R] (Submodule.span R (v '' s))

                                Finsupp.totalOn M v s interprets p : α →₀ R as a linear combination of a subset of the vectors in v, mapping it to the span of those vectors.

                                The subset is indicated by a set s : Set α of indices.

                                Equations
                                Instances For
                                  theorem Finsupp.totalOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (s : Set α) :
                                  theorem Finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : αM} (f : α'α) :
                                  Finsupp.total α' M R (v f) = Finsupp.total α M R v ∘ₗ Finsupp.lmapDomain R R f
                                  theorem Finsupp.total_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : αM} (f : αα') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' l.support)) :
                                  (Finsupp.total α M R v) (Finsupp.comapDomain f l hf) = Finset.sum (Finset.preimage l.support f hf) fun (i : α) => l (f i) v i
                                  theorem Finsupp.total_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset α} {f : αR} (g : αM) (hf : ∀ (a : α), f a 0a s) :
                                  (Finsupp.total α M R g) (Finsupp.onFinset s f hf) = Finset.sum s fun (x : α) => f x g x
                                  def Finsupp.domLCongr {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) :
                                  (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M

                                  An equivalence of domains induces a linear equivalence of finitely supported functions.

                                  This is Finsupp.domCongr as a LinearEquiv. See also LinearMap.funCongrLeft for the case of arbitrary functions.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Finsupp.domLCongr_apply {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) (v : α₁ →₀ M) :
                                    @[simp]
                                    theorem Finsupp.domLCongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
                                    theorem Finsupp.domLCongr_trans {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} {α₃ : Type u_9} (f : α₁ α₂) (f₂ : α₂ α₃) :
                                    Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂ = Finsupp.domLCongr (f.trans f₂)
                                    @[simp]
                                    theorem Finsupp.domLCongr_symm {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (f : α₁ α₂) :
                                    theorem Finsupp.domLCongr_single {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) (i : α₁) (m : M) :
                                    noncomputable def Finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (s : Set α) (t : Set α') (e : s t) :

                                    An equivalence of sets induces a linear equivalence of Finsupps supported on those sets.

                                    Equations
                                    Instances For
                                      def Finsupp.mapRange.linearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
                                      (α →₀ M) →ₗ[R] α →₀ N

                                      Finsupp.mapRange as a LinearMap.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Finsupp.mapRange.linearMap_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : α →₀ M) :
                                        @[simp]
                                        theorem Finsupp.mapRange.linearMap_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
                                        Finsupp.mapRange.linearMap LinearMap.id = LinearMap.id
                                        theorem Finsupp.mapRange.linearMap_comp {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
                                        def Finsupp.mapRange.linearEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :
                                        (α →₀ M) ≃ₗ[R] α →₀ N

                                        Finsupp.mapRange as a LinearEquiv.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem Finsupp.mapRange.linearEquiv_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (g : α →₀ M) :
                                          theorem Finsupp.mapRange.linearEquiv_trans {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) :
                                          @[simp]
                                          theorem Finsupp.mapRange.linearEquiv_toLinearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) :
                                          def Finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) :
                                          (ι →₀ M) ≃ₗ[R] κ →₀ N

                                          An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
                                            (Finsupp.lcongr e₁ e₂) (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m)
                                            @[simp]
                                            theorem Finsupp.lcongr_apply_apply {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) :
                                            ((Finsupp.lcongr e₁ e₂) f) k = e₂ (f (e₁.symm k))
                                            theorem Finsupp.lcongr_symm_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
                                            (LinearEquiv.symm (Finsupp.lcongr e₁ e₂)) (Finsupp.single k n) = Finsupp.single (e₁.symm k) ((LinearEquiv.symm e₂) n)
                                            @[simp]
                                            theorem Finsupp.lcongr_symm {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) :
                                            @[simp]
                                            theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} :
                                            ∀ (a : (α →₀ M) × (β →₀ M)), (LinearEquiv.symm (Finsupp.sumFinsuppLEquivProdFinsupp R)) a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a
                                            @[simp]
                                            theorem Finsupp.sumFinsuppLEquivProdFinsupp_apply {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} :
                                            ∀ (a : α β →₀ M), (Finsupp.sumFinsuppLEquivProdFinsupp R) a = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a
                                            def Finsupp.sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} :
                                            (α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)

                                            The linear equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).

                                            This is the LinearEquiv version of Finsupp.sumFinsuppEquivProdFinsupp.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem Finsupp.fst_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (f : α β →₀ M) (x : α) :
                                              theorem Finsupp.snd_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (f : α β →₀ M) (y : β) :
                                              theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
                                              theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
                                              noncomputable def Finsupp.sigmaFinsuppLEquivPiFinsupp (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : ηType u_10} [AddCommMonoid M] [Module R M] :
                                              ((j : η) × ιs j →₀ M) ≃ₗ[R] (j : η) → ιs j →₀ M

                                              On a Fintype η, Finsupp.split is a linear equivalence between (Σ (j : η), ιs j) →₀ M and (j : η) → (ιs j →₀ M).

                                              This is the LinearEquiv version of Finsupp.sigmaFinsuppAddEquivPiFinsupp.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_apply (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : ηType u_10} [AddCommMonoid M] [Module R M] (f : (j : η) × ιs j →₀ M) (j : η) (i : ιs j) :
                                                ((Finsupp.sigmaFinsuppLEquivPiFinsupp R) f j) i = f { fst := j, snd := i }
                                                @[simp]
                                                theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : ηType u_10} [AddCommMonoid M] [Module R M] (f : (j : η) → ιs j →₀ M) (ji : (j : η) × ιs j) :
                                                noncomputable def Finsupp.finsuppProdLEquiv {α : Type u_7} {β : Type u_8} (R : Type u_9) {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] :
                                                (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M

                                                The linear equivalence between α × β →₀ M and α →₀ β →₀ M.

                                                This is the LinearEquiv version of Finsupp.finsuppProdEquiv.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem Finsupp.finsuppProdLEquiv_apply {α : Type u_7} {β : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] (f : α × β →₀ M) (x : α) (y : β) :
                                                  (((Finsupp.finsuppProdLEquiv R) f) x) y = f (x, y)
                                                  @[simp]
                                                  theorem Finsupp.finsuppProdLEquiv_symm_apply {α : Type u_7} {β : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] (f : α →₀ β →₀ M) (xy : α × β) :
                                                  ((LinearEquiv.symm (Finsupp.finsuppProdLEquiv R)) f) xy = (f xy.1) xy.2

                                                  If R is countable, then any R-submodule spanned by a countable family of vectors is countable.

                                                  Equations
                                                  • =
                                                  def Fintype.total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] :
                                                  (αM) →ₗ[S] (αR) →ₗ[R] M

                                                  Fintype.total R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.total is defined on fintype indexed vectors.

                                                  This map is linear in v if R is commutative, and always linear in f. See note [bundled maps over different rings] for why separate R and S semirings are used.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem Fintype.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : αM) (f : αR) :
                                                    ((Fintype.total R S) v) f = Finset.sum Finset.univ fun (i : α) => f i v i
                                                    @[simp]
                                                    theorem Fintype.total_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : αM) [DecidableEq α] (i : α) (r : R) :
                                                    ((Fintype.total R S) v) (Pi.single i r) = r v i
                                                    theorem Finsupp.total_eq_fintype_total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : αM) (x : αR) :
                                                    theorem Finsupp.total_eq_fintype_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : αM) :
                                                    @[simp]
                                                    theorem Fintype.range_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : αM) :
                                                    theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} {x : M} :
                                                    x Submodule.span R (Set.range v) ∃ (c : αR), (Finset.sum Finset.univ fun (i : α) => c i v i) = x

                                                    An element x lies in the span of v iff it can be written as sum ∑ cᵢ • vᵢ = x.

                                                    theorem top_le_span_range_iff_forall_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} :
                                                    Submodule.span R (Set.range v) ∀ (x : M), ∃ (c : αR), (Finset.sum Finset.univ fun (i : α) => c i v i) = x

                                                    A family v : α → V is generating V iff every element (x : V) can be written as sum ∑ cᵢ • vᵢ = x.

                                                    theorem Span.repr_def (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : (Submodule.span R w)) :
                                                    @[irreducible]
                                                    def Span.repr (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : (Submodule.span R w)) :
                                                    w →₀ R

                                                    Pick some representation of x : span R w as a linear combination in w, using the axiom of choice.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Span.finsupp_total_repr (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {w : Set M} (x : (Submodule.span R w)) :
                                                      (Finsupp.total (w) M R Subtype.val) (Span.repr R w x) = x
                                                      theorem Submodule.finsupp_sum_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {β : Type u_5} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ιβM) (h : ∀ (c : ι), f c 0g c (f c) S) :
                                                      theorem LinearMap.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ιM} (l : ι →₀ R) :
                                                      f ((Finsupp.total ι M R g) l) = (Finsupp.total ι N R (f g)) l
                                                      theorem Submodule.exists_finset_of_mem_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (p : ιSubmodule R M) {m : M} (hm : m ⨆ (i : ι), p i) :
                                                      ∃ (s : Finset ι), m ⨆ i ∈ s, p i
                                                      theorem Submodule.mem_iSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {p : ιSubmodule R M} {m : M} :
                                                      m ⨆ (i : ι), p i ∃ (s : Finset ι), m ⨆ i ∈ s, p i

                                                      Submodule.exists_finset_of_mem_iSup as an iff

                                                      theorem Submodule.mem_sSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {m : M} :
                                                      m sSup S ∃ (s : Finset (Submodule R M)), s S m ⨆ i ∈ s, i
                                                      theorem mem_span_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} :
                                                      x Submodule.span R s ∃ (f : MR), (Finset.sum s fun (i : M) => f i i) = x
                                                      theorem mem_span_set {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :
                                                      m Submodule.span R s ∃ (c : M →₀ R), c.support s (Finsupp.sum c fun (mi : M) (r : R) => r mi) = m

                                                      An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if m can be written as a finite R-linear combination of elements of s. The implementation uses Finsupp.sum.

                                                      theorem mem_span_set' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} :
                                                      m Submodule.span R s ∃ (n : ) (f : Fin nR) (g : Fin ns), (Finset.sum Finset.univ fun (i : Fin n) => f i (g i)) = m

                                                      An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if m can be written as a finite R-linear combination of elements of s. The implementation uses a sum indexed by Fin n for some n.

                                                      theorem span_eq_iUnion_nat {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
                                                      (Submodule.span R s) = ⋃ (n : ), (fun (f : Fin nR × M) => Finset.sum Finset.univ fun (i : Fin n) => (f i).1 (f i).2) '' {f : Fin nR × M | ∀ (i : Fin n), (f i).2 s}

                                                      The span of a subset s is the union over all n of the set of linear combinations of at most n terms belonging to s.

                                                      @[simp]
                                                      theorem Module.subsingletonEquiv_symm_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] :
                                                      ∀ (x : ι →₀ R), (LinearEquiv.symm (Module.subsingletonEquiv R M ι)) x = 0
                                                      @[simp]
                                                      theorem Module.subsingletonEquiv_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] :
                                                      ∀ (x : M), (Module.subsingletonEquiv R M ι) x = 0
                                                      def Module.subsingletonEquiv (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] :

                                                      If Subsingleton R, then M ≃ₗ[R] ι →₀ R for any type ι.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def LinearMap.splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective f) :
                                                        (α →₀ R) →ₗ[R] M

                                                        A surjective linear map to finitely supported functions has a splitting.

                                                        Equations
                                                        Instances For
                                                          theorem LinearMap.splittingOfFinsuppSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective f) :
                                                          f ∘ₗ LinearMap.splittingOfFinsuppSurjective f s = LinearMap.id
                                                          def LinearMap.splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] αR) (s : Function.Surjective f) :
                                                          (αR) →ₗ[R] M

                                                          A surjective linear map to functions on a finite type has a splitting.

                                                          Equations
                                                          Instances For
                                                            theorem LinearMap.splittingOfFunOnFintypeSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] αR) (s : Function.Surjective f) :
                                                            theorem LinearMap.coe_finsupp_sum {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) :
                                                            (Finsupp.sum t g) = (Finsupp.sum t fun (i : ι) (d : γ) => g i d)
                                                            @[simp]
                                                            theorem LinearMap.finsupp_sum_apply {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) (b : M) :
                                                            (Finsupp.sum t g) b = Finsupp.sum t fun (i : ι) (d : γ) => (g i d) b