moduleLeft — Mathlib

English

If α is an additive commutative monoid with an A-action (Module A α), then α inherits an S-action for any subalgebra S ⊆ A by restriction of scalars along S → A.

Русский

Если α — коммутативный аддитивный моноид с действием над A, то α наследует действие над S для любой подалгебры S ⊆ A путём ограничения по отображению S → A.

LaTeX

$$$\forall (S : \text{Subalgebra } R A) (\alpha) [AddCommMonoid \alpha] [Module A \alpha] (s : S) (x : \alpha), s \cdot x = ((s : A) \cdot x)$$$

Lean4

/-- The action by a subalgebra is the action by the underlying algebra. -/
instance moduleLeft [AddCommMonoid α] [Module A α] (S : Subalgebra R A) : Module S α :=
  inferInstanceAs (Module S.toSubsemiring α)

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