Theorems · Theorem · linear algebra

Submodule.span_le

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {p : Submodule R M}, Submodule.span R s ≤ p ↔ s ⊆ ↑p

Defined in

Mathlib.LinearAlgebra.Span.Defs

Cited by

164 results in Mathlib

Foundations

Depth 24 from the axioms, rests on 186 definitions · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule