smul_quot

Mathlib.Algebra.RingQuot

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

English

The quotient carries a scalar action compatible with the base algebra: n • [a] = [n • a].

Русский

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

LaTeX

$$$n \cdot [a] = [n \cdot a]$$$

Lean4

theorem smul_quot [Algebra S R] {n : S} {a : R} : (n • ⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (n • a)⟩ := by rfl

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

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

Разделы

Аффилиация

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