Theorems · Theorem · linear algebra

LinearMap.comp_toSpanSingleton

∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (x : M),
  f ∘ₗ LinearMap.toSpanSingleton R M x = LinearMap.toSpanSingleton R M₂ (f x)

Defined in

Mathlib.LinearAlgebra.Span.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule