instModule

Mathlib.Algebra.Order.Module.Synonym

URI: https://scilib.ai/kg/mathlib#Lex.instModule

English

The Lex construction yields a module structure on β with respect to α.

Русский

Конструкция Lex задаёт модульную структуру β относительно α.

LaTeX

$$$\\text{Module}(\\mathrm{Lex}\\; \\alpha)\\; \\beta$$$

Lean4

instance instModule [Semiring α] [AddCommMonoid β] [Module α β] : Module (Lex α) β :=
  ‹Module α β›

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

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

Разделы

Аффилиация

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