instModule'

Mathlib.Algebra.Order.Module.Synonym

URI: https://scilib.ai/kg/mathlib#OrderDual.instModule'

English

The dual betaᵒᵈ also carries a module structure over α.

Русский

У βᵒᵈ также есть модульная структура над α.

LaTeX

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

Lean4

instance instModule' [Semiring α] [AddCommMonoid β] [Module α β] : Module α βᵒᵈ
    where
  add_smul := add_smul (M := β)
  zero_smul := zero_smul _

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

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

Разделы

Аффилиация

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