Theorems · Theorem · linear algebra

Submodule.span_prod_le

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (s : Set M) (t : Set M'),
  Submodule.span R (s ×ˢ t) ≤ (Submodule.span R s).prod (Submodule.span R t)

Defined in

Mathlib.LinearAlgebra.Span.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule