smul_single'

Mathlib.Algebra.MonoidAlgebra.Defs

URI: https://scilib.ai/kg/mathlib#MonoidAlgebra.smul_single'

← MathLib Explorer

English

A variant of smul_single: r' • single m r = single m (r' * r).

Русский

Вариант smul_single: r' • single m r = single m (r' * r).

LaTeX

$$$ r' \\cdot \\mathrm{single}(m,r) = \\mathrm{single}(m, r' \\ast r) $$$

Lean4

@[to_additive (dont_translate := R) smul_single']
theorem smul_single' (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r) :=
  smul_single ..

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

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

Разделы

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

Аффилиация

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