instSMulOfAlgebra

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instSMulOfAlgebra

English

The quotient carries an S-action compatible with the algebra structure: s · [a] = [s · a].

Русский

Кольцо-остаток имеет действие над скалярами, согласованное с алгебраической структурой: s • [a] = [s • a].

LaTeX

$$$s \cdot [a] = [s \cdot a]$$$

Lean4

instance [Algebra S R] : SMul S (RingQuot r) :=
  ⟨smul r⟩

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

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

Разделы

Аффилиация

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