smul_mem

Mathlib.Algebra.Module.Submodule.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.smul_mem

English

If x ∈ p, then r · x ∈ p for any scalar r in the ring.

Русский

Если x принадлежит p, то и r·x принадлежит p для любого скаляра r из кольца.

LaTeX

$$$ \\forall x \\in p,\\ r x \\in p $$$

Lean4

theorem smul_mem (r : R) (h : x ∈ p) : r • x ∈ p :=
  p.smul_mem' r h

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

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

Разделы

Аффилиация

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