instSMul — Mathlib

English

The quotient M/P has an S-action via the same rule: a • [x] = [a • x]. This is the standard inheritance of the scalar action from M to its quotient by P.

Русский

Фактор-модуль M/P имеет действие S по той же формуле: a • [x] = [a • x]. Это нормальное наследование скалярного действия от M к фактор-модулю.

LaTeX

$$$\forall a \in S,\ \forall [x] \in M/ P,\ a \cdot [x] = [a \cdot x]$$$

Lean4

/-- Shortcut to help the elaborator in the common case. -/
instance instSMul : SMul R (M ⧸ P) :=
  Quotient.instSMul' P

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