Documentation

Mathlib.LinearAlgebra.DFinsupp

Properties of the module Π₀ i, M i #

Given an indexed collection of R-modules M i, the R-module structure on Π₀ i, M i is defined in Data.DFinsupp.

In this file we define LinearMap versions of various maps:

Implementation notes #

This file should try to mirror LinearAlgebra.Finsupp where possible. The API of Finsupp is much more developed, but many lemmas in that file should be eligible to copy over.

Tags #

function with finite support, module, linear algebra

def DFinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) :
((i : s) → M i) →ₗ[R] Π₀ (i : ι), M i

DFinsupp.mk as a LinearMap.

Instances For
    def DFinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) :
    M i →ₗ[R] Π₀ (i : ι), M i

    DFinsupp.single as a LinearMap

    Instances For
      theorem DFinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] ⦃φ : (Π₀ (i : ι), M i) →ₗ[R] N ⦃ψ : (Π₀ (i : ι), M i) →ₗ[R] N (h : ∀ (i : ι) (x : M i), φ (DFinsupp.single i x) = ψ (DFinsupp.single i x)) :
      φ = ψ

      Two R-linear maps from Π₀ i, M i which agree on each single i x agree everywhere.

      theorem DFinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] ⦃φ : (Π₀ (i : ι), M i) →ₗ[R] N ⦃ψ : (Π₀ (i : ι), M i) →ₗ[R] N (h : ∀ (i : ι), LinearMap.comp φ (DFinsupp.lsingle i) = LinearMap.comp ψ (DFinsupp.lsingle i)) :
      φ = ψ

      Two R-linear maps from Π₀ i, M i which agree on each single i x agree everywhere.

      See note [partially-applied ext lemmas]. After apply this lemma, if M = R then it suffices to verify φ (single a 1) = ψ (single a 1).

      def DFinsupp.lapply {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) :
      (Π₀ (i : ι), M i) →ₗ[R] M i

      Interpret fun (f : Π₀ i, M i) ↦ f i as a linear map.

      Instances For
        @[simp]
        theorem DFinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (x : (i : s) → M i) :
        @[simp]
        theorem DFinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (x : M i) :
        @[simp]
        theorem DFinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ιType u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :
        ↑(DFinsupp.lapply i) f = f i
        instance DFinsupp.addCommMonoidOfLinearMap {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] :
        AddCommMonoid (Π₀ (i : ι), M i →ₗ[R] N)

        Typeclass inference can't find DFinsupp.addCommMonoid without help for this case. This instance allows it to be found where it is needed on the LHS of the colon in DFinsupp.moduleOfLinearMap.

        instance DFinsupp.moduleOfLinearMap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : ιType u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] :
        Module S (Π₀ (i : ι), M i →ₗ[R] N)

        Typeclass inference can't find DFinsupp.module without help for this case. This is needed to define DFinsupp.lsum below.

        The cause seems to be an inability to unify the ∀ i, AddCommMonoid (M i →ₗ[R] N) instance that we have with the ∀ i, Zero (M i →ₗ[R] N) instance which appears as a parameter to the DFinsupp type.

        instance DFinsupp.instEquivLikeLinearEquiv {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_8) (M₂ : Type u_9) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
        EquivLike (M ≃ₛₗ[σ] M₂) M M₂
        @[simp]
        theorem DFinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :
        @[simp]
        theorem DFinsupp.lsum_apply_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (a : Π₀ (i : ι), M i) :
        ↑(↑(DFinsupp.lsum S) F) a = ↑(DFinsupp.sumAddHom fun i => LinearMap.toAddMonoidHom (F i)) a
        def DFinsupp.lsum {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] :
        ((i : ι) → M i →ₗ[R] N) ≃ₗ[S] (Π₀ (i : ι), M i) →ₗ[R] N

        The DFinsupp version of Finsupp.lsum.

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

        Instances For
          theorem DFinsupp.lsum_single {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ιType u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i) :
          ↑(↑(DFinsupp.lsum S) F) (DFinsupp.single i x) = ↑(F i) x

          While simp can prove this, it is often convenient to avoid unfolding lsum into sumAddHom with DFinsupp.lsum_apply_apply.

          Bundled versions of DFinsupp.mapRange #

          The names should match the equivalent bundled Finsupp.mapRange definitions.

          theorem DFinsupp.mapRange_smul {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (r : R) (hf' : ∀ (i : ι) (x : β₁ i), f i (r x) = r f i x) (g : Π₀ (i : ι), β₁ i) :
          @[simp]
          theorem DFinsupp.mapRange.linearMap_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) :
          ↑(DFinsupp.mapRange.linearMap f) x = DFinsupp.mapRange (fun i x => ↑(f i) x) (_ : ∀ (i : ι), ↑(f i) 0 = 0) x
          def DFinsupp.mapRange.linearMap {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) :
          (Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i

          DFinsupp.mapRange as a LinearMap.

          Instances For
            @[simp]
            theorem DFinsupp.mapRange.linearMap_id {ι : Type u_1} {R : Type u_2} [dec_ι : DecidableEq ι] [Semiring R] {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₂ i)] :
            (DFinsupp.mapRange.linearMap fun i => LinearMap.id) = LinearMap.id
            theorem DFinsupp.mapRange.linearMap_comp {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ιType u_6} {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (f₂ : (i : ι) → β i →ₗ[R] β₁ i) :
            theorem DFinsupp.sum_mapRange_index.linearMap {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] [(i : ι) → (x : β₁ i) → Decidable (x 0)] [(i : ι) → (x : β₂ i) → Decidable (x 0)] {f : (i : ι) → β₁ i →ₗ[R] β₂ i} {h : (i : ι) → β₂ i →ₗ[R] N} {l : Π₀ (i : ι), β₁ i} :
            ↑(↑(DFinsupp.lsum ) h) (↑(DFinsupp.mapRange.linearMap f) l) = ↑(↑(DFinsupp.lsum ) fun i => LinearMap.comp (h i) (f i)) l
            @[simp]
            theorem DFinsupp.mapRange.linearEquiv_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) :
            ↑(DFinsupp.mapRange.linearEquiv e) x = DFinsupp.mapRange (fun i x => ↑(e i) x) (_ : ∀ (i : ι), ↑(e i) 0 = 0) x
            def DFinsupp.mapRange.linearEquiv {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
            (Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

            DFinsupp.mapRange.linearMap as a LinearEquiv.

            Instances For
              @[simp]
              theorem DFinsupp.mapRange.linearEquiv_refl {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → Module R (β₁ i)] :
              (DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl R (Π₀ (i : ι), β₁ i)
              theorem DFinsupp.mapRange.linearEquiv_trans {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ιType u_6} {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β i ≃ₗ[R] β₁ i) (f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
              @[simp]
              theorem DFinsupp.mapRange.linearEquiv_symm {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ιType u_7} {β₂ : ιType u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
              def DFinsupp.coprodMap {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) :
              (Π₀ (i : ι), M i) →ₗ[R] N

              Given a family of linear maps f i : M i →ₗ[R] N, we can form a linear map (Π₀ i, M i) →ₗ[R] N which sends x : Π₀ i, M i to the sum over i of f i applied to x i. This is the map coming from the universal property of Π₀ i, M i as the coproduct of the M i. See also LinearMap.coprod for the binary product version.

              Instances For
                theorem DFinsupp.coprodMap_apply {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [(x : N) → Decidable (x 0)] (f : (i : ι) → M i →ₗ[R] N) (x : Π₀ (i : ι), M i) :
                ↑(DFinsupp.coprodMap f) x = DFinsupp.sum (DFinsupp.mapRange (fun i => ↑(f i)) (_ : ∀ (x : ι), ↑(f x) 0 = 0) x) fun x => id
                theorem DFinsupp.coprodMap_apply_single {ι : Type u_1} {R : Type u_2} {M : ιType u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i) :
                ↑(DFinsupp.coprodMap f) (DFinsupp.single i x) = ↑(f i) x
                theorem Submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β : ιType u_6} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (S : Submodule R N) (f : Π₀ (i : ι), β i) (g : (i : ι) → β iN) (h : ∀ (c : ι), f c 0g c (f c) S) :
                theorem Submodule.dfinsupp_sumAddHom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β : ιType u_6} [(i : ι) → AddZeroClass (β i)] (S : Submodule R N) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ N) (h : ∀ (c : ι), f c 0↑(g c) (f c) S) :
                theorem Submodule.iSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιSubmodule R N) :

                The supremum of a family of submodules is equal to the range of DFinsupp.lsum; that is every element in the iSup can be produced from taking a finite number of non-zero elements of p i, coercing them to N, and summing them.

                theorem Submodule.biSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιProp) [DecidablePred p] (S : ιSubmodule R N) :
                ⨆ (i : ι) (x : p i), S i = LinearMap.range (LinearMap.comp (↑(DFinsupp.lsum ) fun i => Submodule.subtype (S i)) (DFinsupp.filterLinearMap R (fun i => { x // x S i }) p))

                The bounded supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom composed with DFinsupp.filter_add_monoid_hom; that is, every element in the bounded iSup can be produced from taking a finite number of non-zero elements from the S i that satisfy p i, coercing them to γ, and summing them.

                theorem Submodule.mem_iSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιSubmodule R N) (x : N) :
                x iSup p f, ↑(↑(DFinsupp.lsum ) fun i => Submodule.subtype (p i)) f = x
                theorem Submodule.mem_iSup_iff_exists_dfinsupp' {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιSubmodule R N) [(i : ι) → (x : { x // x p i }) → Decidable (x 0)] (x : N) :
                x iSup p f, (DFinsupp.sum f fun i xi => xi) = x

                A variant of Submodule.mem_iSup_iff_exists_dfinsupp with the RHS fully unfolded.

                theorem Submodule.mem_biSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιProp) [DecidablePred p] (S : ιSubmodule R N) (x : N) :
                x ⨆ (i : ι) (x : p i), S i f, ↑(↑(DFinsupp.lsum ) fun i => Submodule.subtype (S i)) (DFinsupp.filter p f) = x
                theorem Submodule.mem_iSup_finset_iff_exists_sum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {s : Finset ι} (p : ιSubmodule R N) (a : N) :
                a ⨆ (i : ι) (_ : i s), p i μ, (Finset.sum s fun i => ↑(μ i)) = a
                theorem CompleteLattice.independent_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιSubmodule R N) :
                CompleteLattice.Independent p ∀ (i : ι) (x : { x // x p i }) (v : Π₀ (i : ι), { x // x p i }), ↑(↑(DFinsupp.lsum ) fun i => Submodule.subtype (p i)) (DFinsupp.erase i v) = xx = 0

                Independence of a family of submodules can be expressed as a quantifier over DFinsupps.

                This is an intermediate result used to prove CompleteLattice.independent_of_dfinsupp_lsum_injective and CompleteLattice.Independent.dfinsupp_lsum_injective.

                theorem CompleteLattice.lsum_comp_mapRange_toSpanSingleton {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] [(m : R) → Decidable (m 0)] (p : ιSubmodule R N) {v : ιN} (hv : ∀ (i : ι), v i p i) :
                LinearMap.comp (↑(DFinsupp.lsum ) fun i => Submodule.subtype (p i)) (LinearMap.comp (DFinsupp.mapRange.linearMap fun i => LinearMap.toSpanSingleton R { x // x p i } { val := v i, property := hv i }) ↑(finsuppLequivDFinsupp R)) = Finsupp.total ι N R v

                Combining DFinsupp.lsum with LinearMap.toSpanSingleton is the same as Finsupp.total

                theorem CompleteLattice.Independent.dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ιSubmodule R N} (h : CompleteLattice.Independent p) :

                The canonical map out of a direct sum of a family of submodules is injective when the submodules are CompleteLattice.Independent.

                Note that this is not generally true for [Semiring R], for instance when A is the -submodules of the positive and negative integers.

                See Counterexamples/DirectSumIsInternal.lean for a proof of this fact.

                The canonical map out of a direct sum of a family of additive subgroups is injective when the additive subgroups are CompleteLattice.Independent.

                A family of submodules over an additive group are independent if and only iff DFinsupp.lsum applied with Submodule.subtype is injective.

                Note that this is not generally true for [Semiring R]; see CompleteLattice.Independent.dfinsupp_lsum_injective for details.

                A family of additive subgroups over an additive group are independent if and only if DFinsupp.sumAddHom applied with AddSubgroup.subtype is injective.

                theorem CompleteLattice.Independent.linearIndependent {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] (p : ιSubmodule R N) (hp : CompleteLattice.Independent p) {v : ιN} (hv : ∀ (i : ι), v i p i) (hv' : ∀ (i : ι), v i 0) :

                If a family of submodules is Independent, then a choice of nonzero vector from each submodule forms a linearly independent family.

                See also CompleteLattice.Independent.linearIndependent'.

                theorem CompleteLattice.independent_iff_linearIndependent_of_ne_zero {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] {v : ιN} (h_ne_zero : ∀ (i : ι), v i 0) :