English
Let p be a SubMulAction of M with a group G acting on R and M so that there is a scalar tower G → R → M. Then for every g ∈ G and every x ∈ M, g · x ∈ p iff x ∈ p. Membership in p is invariant under the G-action.
Русский
Пусть p — SubMulAction над M с действием группы G на R и M через башню скаляров. Тогда для любого g ∈ G и любого x ∈ M верно: g · x ∈ p тогда и только тогда, когда x ∈ p. Инвариантность принадлежности p относительно действия G.
LaTeX
$$$ \\forall g : G, \\forall x : M, \\\\ g \\cdot x \\in p \\iff x \\in p. $$$
Lean4
@[to_additive (attr := simp)]
theorem smul_mem_iff' {G} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} :
g • x ∈ p ↔ x ∈ p :=
⟨fun h => inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩
