Theorems · Theorem · linear algebra

LinearMap.span_inl_union_inr

∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {s : Set M} {t : Set M₂},
  Submodule.span R (⇑(LinearMap.inl R M M₂) '' s ∪ ⇑(LinearMap.inr R M M₂) '' t) =
    (Submodule.span R s).prod (Submodule.span R t)

Defined in

Mathlib.LinearAlgebra.Prod

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule