Theorems · Definition · linear algebra

Submodule.span

(R : Type u_1) →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set M → Submodule R M

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Defined in

Mathlib.LinearAlgebra.Span.Defs

Cited by

1,504 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 103 definitions · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule