instModule

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

English

There is a module structure on S over R induced from A.

Русский

У S существует модульная структура над R, полученная от A.

LaTeX

$$Module R S$$

Lean4

instance instModule : Module R S :=
  S.module'

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

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

Разделы

Аффилиация

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