coe_mop_smul

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

English

The Mop action on I satisfies (r • x) = x · r.unop in R.

Русский

Действие Mop на I удовлетворяет (r · x) = x · r.unop в кольце R.

LaTeX

$$$ (r \\cdot x) = x \\cdot r^{\\mathrm{unop}} $$$

Lean4

@[simp]
theorem coe_mop_smul {r : Rᵐᵒᵖ} {x : I} : (r • x : R) = (x : R) * r.unop :=
  rfl

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

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

Разделы

Аффилиация

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