toSpanSingleton_eq_algebra_linearMap

English

The span-singleton construction at 1 recovers the canonical linear map defining the R-action on A; i.e., the map toSpanSingleton R A 1 equals Algebra.linearMap R A.

Русский

Конструкция span-singleton в единице возвращает каноническое линейное отображение, задающее действие R на A; то есть toSpanSingleton R A 1 равняется Algebra.linearMap R A.

LaTeX

$$$\operatorname{toSpanSingleton}(R,A)(1)=\operatorname{Algebra.linearMap}(R,A).$$$

Lean4

theorem toSpanSingleton_eq_algebra_linearMap : toSpanSingleton R A 1 = Algebra.linearMap R A := by ext; simp

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