rightModule

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

English

The set I, viewed as a subset with opposite action, carries a right module structure over MulOpposite R.

Русский

Множество I, рассматриваемое как правый модуль над MulOpposite R.

LaTeX

$$$I \\text{ is a module over } MulOpposite\\,R$$$

Lean4

instance rightModule : Module Rᵐᵒᵖ I :=
  Function.Injective.module _ (coeAddMonoidHom I) Subtype.coe_injective fun _ _ ↦ rfl

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

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

Разделы

Аффилиация

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