smul_eq_mul

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.id.smul_eq_mul

English

The scalar action of R on itself coincides with multiplication: for all x,y ∈ R, x • y = x y.

Русский

Скалярное действие элемента кольца R на себя совпадает с умножением: для всех x,y ∈ R выполняется x • y = x y.

LaTeX

$$$\\forall x,y \\in R,\\; x \\cdot y = x y$$$

Lean4

@[simp]
theorem smul_eq_mul (x y : R) : x • y = x * y :=
  rfl

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

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

Разделы

Аффилиация

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