coe_smul

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.coe_smul

English

The scalar action of R on I coincides with the multiplication in R: (r · x) = r x for r ∈ R, x ∈ I.

Русский

Скалярное действие кольца R на I совпадает с умножением в R: (r · x) = r x для r ∈ R, x ∈ I.

LaTeX

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

Lean4

@[simp]
theorem coe_smul {r : R} {x : I} : (r • x : R) = r * (x : R) :=
  rfl

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

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

Разделы

Аффилиация

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