smul_of_tower_mem — Mathlib

English

If a submodule is stable under a tower of scalar actions, then scalar multiplication by the outer scalar preserves membership.

Русский

Если подмодуль стабилен относительно каскада скалярных действий, умножение на внешний скаляр сохраняет членство.

LaTeX

$$$ \\forall x \\in p,\\ r \\cdot x \\in p \\quad \\text{under } (S,R,M) \\text{ tower}$$

Lean4

theorem smul_of_tower_mem [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) : r • x ∈ p :=
  p.toSubMulAction.smul_of_tower_mem r h

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