toSpanSingleton_smul — Mathlib

English

If r acts on x via a monoid S with a distributive action, then toSpanSingleton respects SMul: toSpanSingleton(r•x) = r•toSpanSingleton(x).

Русский

Пусть действует скаляр r на x; тогда toSpanSingleton(r•x) = r•toSpanSingleton(x).

LaTeX

$$$toSpanSingleton\,R\,M\ (r \cdot x) = r \cdot toSpanSingleton\,R\,M\ x$$$

Lean4

theorem toSpanSingleton_smul {S : Type*} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (r : S) (x : M) :
    toSpanSingleton R M (r • x) = r • toSpanSingleton R M x := by ext; simp

Похожие утверждения