smul_mul_assoc

Mathlib.Algebra.Algebra.Defs

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

← MathLib Explorer

English

For r ∈ R and x,y ∈ A, r • x · y = r • (x · y).

Русский

Для r ∈ R и x,y ∈ A выполняется r • x · y = r • (x · y).

LaTeX

$$$r \cdot x \cdot y = r \cdot (x \cdot y)$$$

Lean4

/-- This is just a special case of the global `smul_mul_assoc` lemma that requires less typeclass
search (and was here first). -/
@[simp]
protected theorem smul_mul_assoc (r : R) (x y : A) : r • x * y = r • (x * y) :=
  smul_mul_assoc r x y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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