smul_def

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.smul_def

English

In an R-algebra A, the action of an element r ∈ R on x ∈ A is given by r • x = algebraMap R A r · x.

Русский

В алгебре над R действие элемента r ∈ R на x ∈ A определяется как r • x = algebraMap(R,A)(r) · x.

LaTeX

$$$r \cdot x = \operatorname{algebraMap}(R,A)(r)\,x$$$

Lean4

theorem smul_def (r : R) (x : A) : r • x = algebraMap R A r * x :=
  Algebra.smul_def' r x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru