hasNatSMul

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#LocalizedModule.hasNatSMul

English

There is a natural-number scalar action on LocalizedModule defined by nsmul.

Русский

Существует действие скаляров из натурального числа на LocalizedModule, заданное nsmul.

LaTeX

$$$\\text{instance hasNatSMul} : SMul \\mathbb{N} (LocalizedModule S M)$ with $n \\mapsto nsmulRec(n)$.$$

Lean4

instance hasNatSMul : SMul ℕ (LocalizedModule S M) where smul n := nsmulRec n

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

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

Разделы

Аффилиация

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