Theorems · Theorem · linear algebra

Module.Basis.mem_span_iff_repr_mem

∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [IsDomain R] [inst_2 : Ring S]
  [Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M] [inst_7 : Module R M]
  [IsScalarTower R S M] [Module.IsTorsionFree R S] (b : Module.Basis ι S M) (m : M),
  m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)

Let b be an S-basis of M. Then m : M lies in the R-module spanned by b iff all the coordinates of m on the basis b are in R (see Basis.mem_span for the case R = S).

Defined in

Mathlib.LinearAlgebra.Basis.Submodule

Cited by

6 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainRingNontrivialAddCommGroupAlgebraModuleModuleIsScalarTowerModule.IsTorsionFree