smul_of_tower_mem

Mathlib.GroupTheory.GroupAction.SubMulAction

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

English

If x ∈ p, then s•x ∈ p for any s ∈ S under an appropriate tower.

Русский

Если x ∈ p, то s•x ∈ p для любого s ∈ S с учётом корректной башни.

LaTeX

$$$\\forall s:\\ S, \\forall x:\\ x \\in p \\Rightarrow s \\cdot x \\in p$$$

Lean4

@[to_additive]
theorem smul_of_tower_mem (s : S) {x : M} (h : x ∈ p) : s • x ∈ p :=
  by
  rw [← one_smul R x, ← smul_assoc]
  exact p.smul_mem _ h

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

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

Разделы

Аффилиация

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