toStarModuleInt

Mathlib.Algebra.Star.Basic

URI: https://scilib.ai/kg/mathlib#StarAddMonoid.toStarModuleInt

English

Given a star-additive monoid α, there is a StarModule structure of α over ℤ, with the action by z-scaling.

Русский

Для α существует структура StarModule над ℤ, с действием целочисленного масштаба.

LaTeX

$$$$ \text{StarModule}_{\mathbb{Z}} \; \alpha. $$$$

Lean4

instance toStarModuleInt {α} [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where star_smul := star_zsmul

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

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

Разделы

Аффилиация

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