Theorems · Theorem · linear algebra

Submodule.span_span_of_tower

∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [IsScalarTower R S M],
  Submodule.span S ↑(Submodule.span R s) = Submodule.span S s

Taking the span by a large ring of the span by the small ring is the same as taking the span by just the large ring.

Defined in

Mathlib.LinearAlgebra.Span.Basic

Cited by

18 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModuleSemiringSMulModuleIsScalarTower