smul_mem_iff' — Mathlib

English

For a group acting on M, the submodule p is invariant under the action: g·x ∈ p iff x ∈ p for all x ∈ M.

Русский

Для группы, действующей на M, подмодуль p инвариантен относительно действия: g·x ∈ p тогда и только тогда, когда x ∈ p.

LaTeX

$$$ \\forall g \\in G,\\forall x \\in M,\\ g·x \\in p \\iff x \\in p $$$

Lean4

@[simp]
theorem smul_mem_iff' [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) : g • x ∈ p ↔ x ∈ p :=
  p.toSubMulAction.smul_mem_iff' g

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