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 v.sum h = v.sum 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₂} :
((c v).sum fun (a : α) => (h a)) = c v.sum 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
  • Finsupp.linearEquivFunOnFinite R M α = { toFun := DFunLike.coe, map_add' := , map_smul' := , invFun := Finsupp.equivFunOnFinite.invFun, left_inv := , right_inv := }
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) :
    (Finsupp.linearEquivFunOnFinite R M α).symm f = f
    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]
      theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {α : Type u_4} [Unique α] (m : M) :
      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'_iff {α : 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} :
        φ = ψ ∀ (a : α), φ ∘ₗ Finsupp.lsingle a = ψ ∘ₗ Finsupp.lsingle a
        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 = { 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
              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 ∘ₗ (Finsupp.supported M R s).subtype = 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) => d.sum 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 = l.sum 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 : α) :
                      (Finsupp.lsum S).symm f x = f ∘ₗ Finsupp.lsingle 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
                      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) :
                        (Finsupp.lift M R X).symm f x = f (Finsupp.single x 1)
                        @[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 = g.sum 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
                        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) :
                          (Finsupp.llift M R S X).symm f x = f (Finsupp.single x 1)
                          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.linearCombination {α : 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 a linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

                              Equations
                              Instances For
                                @[deprecated Finsupp.linearCombination]
                                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

                                Alias of Finsupp.linearCombination.


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

                                Equations
                                Instances For
                                  theorem Finsupp.linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (l : α →₀ R) :
                                  (Finsupp.linearCombination R v) l = l.sum fun (i : α) (a : R) => a v i
                                  @[deprecated Finsupp.linearCombination_apply]
                                  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.linearCombination R v) l = l.sum fun (i : α) (a : R) => a v i

                                  Alias of Finsupp.linearCombination_apply.

                                  theorem Finsupp.linearCombination_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.linearCombination R v) l = is, l i v i
                                  @[deprecated Finsupp.linearCombination_apply_of_mem_supported]
                                  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.linearCombination R v) l = is, l i v i

                                  Alias of Finsupp.linearCombination_apply_of_mem_supported.

                                  @[simp]
                                  theorem Finsupp.linearCombination_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (c : R) (a : α) :
                                  @[deprecated Finsupp.linearCombination_single]
                                  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 : α) :

                                  Alias of Finsupp.linearCombination_single.

                                  theorem Finsupp.linearCombination_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : α →₀ R) :
                                  @[deprecated Finsupp.linearCombination_zero_apply]
                                  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) :

                                  Alias of Finsupp.linearCombination_zero_apply.

                                  @[simp]
                                  theorem Finsupp.linearCombination_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :
                                  @[deprecated Finsupp.linearCombination_zero]
                                  theorem Finsupp.total_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] :

                                  Alias of Finsupp.linearCombination_zero.

                                  theorem Finsupp.apply_linearCombination {α : 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) :
                                  @[deprecated Finsupp.apply_linearCombination]
                                  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) :

                                  Alias of Finsupp.apply_linearCombination.

                                  theorem Finsupp.apply_linearCombination_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) :
                                  @[deprecated Finsupp.apply_linearCombination_id]
                                  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) :

                                  Alias of Finsupp.apply_linearCombination_id.

                                  theorem Finsupp.linearCombination_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.linearCombination R v) l = l default v default
                                  @[deprecated Finsupp.linearCombination_unique]
                                  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.linearCombination R v) l = l default v default

                                  Alias of Finsupp.linearCombination_unique.

                                  @[deprecated Finsupp.linearCombination_surjective]
                                  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) :

                                  Alias of Finsupp.linearCombination_surjective.

                                  theorem Finsupp.linearCombination_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) :
                                  @[deprecated Finsupp.linearCombination_range]
                                  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) :

                                  Alias of Finsupp.linearCombination_range.

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

                                  @[deprecated Finsupp.linearCombination_id_surjective]

                                  Alias of Finsupp.linearCombination_id_surjective.


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

                                  @[deprecated Finsupp.range_linearCombination]
                                  theorem Finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} :

                                  Alias of Finsupp.range_linearCombination.

                                  theorem Finsupp.lmapDomain_linearCombination {α : 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)) :
                                  @[deprecated Finsupp.lmapDomain_linearCombination]
                                  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)) :

                                  Alias of Finsupp.lmapDomain_linearCombination.

                                  theorem Finsupp.linearCombination_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 : αα') :
                                  @[deprecated Finsupp.linearCombination_comp_lmapDomain]
                                  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 : αα') :

                                  Alias of Finsupp.linearCombination_comp_lmapDomain.

                                  @[simp]
                                  theorem Finsupp.linearCombination_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) :
                                  @[deprecated Finsupp.linearCombination_embDomain]
                                  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) :

                                  Alias of Finsupp.linearCombination_embDomain.

                                  @[simp]
                                  theorem Finsupp.linearCombination_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) :
                                  @[deprecated Finsupp.linearCombination_mapDomain]
                                  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) :

                                  Alias of Finsupp.linearCombination_mapDomain.

                                  @[simp]
                                  theorem Finsupp.linearCombination_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) :
                                  @[deprecated Finsupp.linearCombination_equivMapDomain]
                                  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) :

                                  Alias of Finsupp.linearCombination_equivMapDomain.

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

                                  @[deprecated Finsupp.span_eq_range_linearCombination]
                                  theorem Finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

                                  Alias of Finsupp.span_eq_range_linearCombination.


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

                                  theorem Finsupp.mem_span_iff_linearCombination {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.linearCombination R Subtype.val) l = x
                                  @[deprecated Finsupp.mem_span_iff_linearCombination]
                                  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.linearCombination R Subtype.val) l = x

                                  Alias of Finsupp.mem_span_iff_linearCombination.

                                  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), (c.sum fun (i : α) (a : R) => a v i) = x
                                  theorem Finsupp.span_image_eq_map_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (s : Set α) :
                                  @[deprecated Finsupp.span_image_eq_map_linearCombination]
                                  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 α) :

                                  Alias of Finsupp.span_image_eq_map_linearCombination.

                                  theorem Finsupp.mem_span_image_iff_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} {s : Set α} {x : M} :
                                  @[deprecated Finsupp.mem_span_image_iff_linearCombination]
                                  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} :

                                  Alias of Finsupp.mem_span_image_iff_linearCombination.

                                  theorem Finsupp.linearCombination_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.linearCombination R v) f = f none v none + (Finsupp.linearCombination R (v some)) f.some
                                  @[deprecated Finsupp.linearCombination_option]
                                  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.linearCombination R v) f = f none v none + (Finsupp.linearCombination R (v some)) f.some

                                  Alias of Finsupp.linearCombination_option.

                                  theorem Finsupp.linearCombination_linearCombination {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) :
                                  @[deprecated Finsupp.linearCombination_linearCombination]
                                  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) :

                                  Alias of Finsupp.linearCombination_linearCombination.

                                  @[simp]
                                  theorem Finsupp.linearCombination_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0M) :
                                  @[deprecated Finsupp.linearCombination_fin_zero]
                                  theorem Finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0M) :

                                  Alias of Finsupp.linearCombination_fin_zero.

                                  def Finsupp.linearCombinationOn (α : 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.linearCombinationOn 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
                                    @[deprecated Finsupp.linearCombinationOn]
                                    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))

                                    Alias of Finsupp.linearCombinationOn.


                                    Finsupp.linearCombinationOn 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.linearCombinationOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : αM} (s : Set α) :
                                      @[deprecated Finsupp.linearCombinationOn_range]
                                      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 α) :

                                      Alias of Finsupp.linearCombinationOn_range.

                                      theorem Finsupp.linearCombination_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 : α'α) :
                                      @[deprecated Finsupp.linearCombination_comp]
                                      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 : α'α) :

                                      Alias of Finsupp.linearCombination_comp.

                                      theorem Finsupp.linearCombination_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.linearCombination R v) (Finsupp.comapDomain f l hf) = il.support.preimage f hf, l (f i) v i
                                      @[deprecated Finsupp.linearCombination_comapDomain]
                                      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.linearCombination R v) (Finsupp.comapDomain f l hf) = il.support.preimage f hf, l (f i) v i

                                      Alias of Finsupp.linearCombination_comapDomain.

                                      theorem Finsupp.linearCombination_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.linearCombination R g) (Finsupp.onFinset s f hf) = xs, f x g x
                                      @[deprecated Finsupp.linearCombination_onFinset]
                                      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.linearCombination R g) (Finsupp.onFinset s f hf) = xs, f x g x

                                      Alias of Finsupp.linearCombination_onFinset.

                                      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) :
                                            @[simp]
                                            theorem Finsupp.mapRange.linearMap_toAddMonoidHom {α : 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) :
                                            (Finsupp.mapRange.linearMap f).toAddMonoidHom = Finsupp.mapRange.addMonoidHom f.toAddMonoidHom
                                            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
                                            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_symm {α : 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) :
                                              @[simp]
                                              theorem Finsupp.mapRange.linearEquiv_toAddEquiv {α : 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) :
                                              @[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) :
                                                (Finsupp.lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm 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) :
                                                (Finsupp.lcongr e₁ e₂).symm = Finsupp.lcongr e₁.symm e₂.symm
                                                @[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
                                                @[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)), (Finsupp.sumFinsuppLEquivProdFinsupp R).symm a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun 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 j, 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) :
                                                    ((Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f) ji = (f ji.fst) ji.snd
                                                    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
                                                    • Finsupp.finsuppProdLEquiv R = { toFun := Finsupp.finsuppProdEquiv.toFun, map_add' := , map_smul' := , invFun := Finsupp.finsuppProdEquiv.invFun, left_inv := , right_inv := }
                                                    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 : α × β) :
                                                      ((Finsupp.finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2
                                                      instance Finsupp.instCountableSubtypeMemSubmoduleSpanRange {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} [Countable R] [Countable ι] (v : ιM) :

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

                                                      Equations
                                                      • =
                                                      def Fintype.linearCombination {α : 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.linearCombination R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.linearCombination 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
                                                      • Fintype.linearCombination R S = { toFun := fun (v : αM) => { toFun := fun (f : αR) => i : α, f i v i, map_add' := , map_smul' := }, map_add' := , map_smul' := }
                                                      Instances For
                                                        @[deprecated Fintype.linearCombination]
                                                        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

                                                        Alias of Fintype.linearCombination.


                                                        Fintype.linearCombination R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.linearCombination 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
                                                        Instances For
                                                          theorem Fintype.linearCombination_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.linearCombination R S) v) f = i : α, f i v i
                                                          @[deprecated Fintype.linearCombination_apply]
                                                          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.linearCombination R S) v) f = i : α, f i v i

                                                          Alias of Fintype.linearCombination_apply.

                                                          @[simp]
                                                          theorem Fintype.linearCombination_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) :
                                                          @[deprecated Fintype.linearCombination_apply_single]
                                                          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) :

                                                          Alias of Fintype.linearCombination_apply_single.

                                                          theorem Finsupp.linearCombination_eq_fintype_linearCombination_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) :
                                                          @[deprecated Finsupp.linearCombination_eq_fintype_linearCombination_apply]
                                                          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) :

                                                          Alias of Finsupp.linearCombination_eq_fintype_linearCombination_apply.

                                                          theorem Finsupp.linearCombination_eq_fintype_linearCombination {α : 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) :
                                                          @[deprecated Finsupp.linearCombination_eq_fintype_linearCombination]
                                                          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) :

                                                          Alias of Finsupp.linearCombination_eq_fintype_linearCombination.

                                                          @[simp]
                                                          theorem Fintype.range_linearCombination {α : 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) :
                                                          @[deprecated Fintype.range_linearCombination]
                                                          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) :

                                                          Alias of Fintype.range_linearCombination.

                                                          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), 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), 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)) :
                                                          Span.repr R w x = .choose
                                                          @[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, ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem Span.finsupp_linearCombination_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.linearCombination R Subtype.val) (Span.repr R w x) = x
                                                            @[deprecated Span.finsupp_linearCombination_repr]
                                                            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.linearCombination R Subtype.val) (Span.repr R w x) = x

                                                            Alias of Span.finsupp_linearCombination_repr.

                                                            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) :
                                                            f.sum g S
                                                            theorem LinearMap.map_finsupp_linearCombination {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) :
                                                            @[deprecated LinearMap.map_finsupp_linearCombination]
                                                            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) :

                                                            Alias of LinearMap.map_finsupp_linearCombination.

                                                            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 is, 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 is, 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 is, 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), is, 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 (c.sum 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), 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) => 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), (Module.subsingletonEquiv R M ι).symm 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
                                                            • Module.subsingletonEquiv R M ι = { toFun := fun (x : M) => 0, map_add' := , map_smul' := , invFun := fun (x : ι →₀ R) => 0, left_inv := , right_inv := }
                                                            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
                                                              • f.splittingOfFinsuppSurjective s = (Finsupp.lift M R α) fun (x : α) => .choose
                                                              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 ∘ₗ f.splittingOfFinsuppSurjective s = LinearMap.id
                                                                theorem LinearMap.leftInverse_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) :
                                                                Function.LeftInverse f (f.splittingOfFinsuppSurjective s)
                                                                theorem LinearMap.splittingOfFinsuppSurjective_injective {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) :
                                                                Function.Injective (f.splittingOfFinsuppSurjective s)
                                                                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) :
                                                                  f ∘ₗ f.splittingOfFunOnFintypeSurjective s = LinearMap.id
                                                                  theorem LinearMap.leftInverse_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) :
                                                                  Function.LeftInverse f (f.splittingOfFunOnFintypeSurjective s)
                                                                  theorem LinearMap.splittingOfFunOnFintypeSurjective_injective {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) :
                                                                  Function.Injective (f.splittingOfFunOnFintypeSurjective s)
                                                                  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₂) :
                                                                  (t.sum g) = (t.sum 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) :
                                                                  (t.sum g) b = t.sum fun (i : ι) (d : γ) => (g i d) b
                                                                  def Submodule.mulLeftMap {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5} (m : ιM) :
                                                                  (ι →₀ N) →ₗ[R] S

                                                                  If M and N are submodules of an R-algebra S, m : ι → M is a family of elements, then there is an R-linear map from ι →₀ N to S which maps { n_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

                                                                  Equations
                                                                  Instances For
                                                                    theorem Submodule.mulLeftMap_apply {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M : Submodule R S} {N : Submodule R S} {ι : Type u_5} (m : ιM) (n : ι →₀ N) :
                                                                    (Submodule.mulLeftMap N m) n = n.sum fun (i : ι) (n : N) => (m i) * n
                                                                    @[simp]
                                                                    theorem Submodule.mulLeftMap_apply_single {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M : Submodule R S} {N : Submodule R S} {ι : Type u_5} (m : ιM) (i : ι) (n : N) :
                                                                    (Submodule.mulLeftMap N m) (Finsupp.single i n) = (m i) * n
                                                                    def Submodule.mulRightMap {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] (M : Submodule R S) {N : Submodule R S} {ι : Type u_5} (n : ιN) :
                                                                    (ι →₀ M) →ₗ[R] S

                                                                    If M and N are submodules of an R-algebra S, n : ι → N is a family of elements, then there is an R-linear map from ι →₀ M to S which maps { m_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

                                                                    Equations
                                                                    Instances For
                                                                      theorem Submodule.mulRightMap_apply {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] {M : Submodule R S} {N : Submodule R S} {ι : Type u_5} (n : ιN) (m : ι →₀ M) :
                                                                      (M.mulRightMap n) m = m.sum fun (i : ι) (m : M) => m * (n i)
                                                                      @[simp]
                                                                      theorem Submodule.mulRightMap_apply_single {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] {M : Submodule R S} {N : Submodule R S} {ι : Type u_5} (n : ιN) (i : ι) (m : M) :
                                                                      (M.mulRightMap n) (Finsupp.single i m) = m * (n i)
                                                                      theorem Submodule.mulLeftMap_eq_mulRightMap_of_commute {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5} (m : ιM) (hc : ∀ (i : ι) (n : N), Commute (m i) n) :
                                                                      Submodule.mulLeftMap N m = N.mulRightMap m
                                                                      theorem Submodule.mulLeftMap_eq_mulRightMap {R : Type u_1} [Semiring R] {S : Type u_5} [CommSemiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] [IsScalarTower R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_6} (m : ιM) :
                                                                      Submodule.mulLeftMap N m = N.mulRightMap m