smul_mem

Mathlib.GroupTheory.GroupAction.SubMulAction

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

English

If x ∈ p and r ∈ R, then r•x ∈ p.

Русский

Если x ∈ p и r ∈ R, то r•x ∈ p.

LaTeX

$$$\\forall r \\in R, \\forall x \\in p:\\ r \\cdot x \\in p$$$

Lean4

@[to_additive]
theorem smul_mem (r : R) (h : x ∈ p) : r • x ∈ p :=
  p.smul_mem' r h

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

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

Разделы

Аффилиация

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