smul_mem_smul_iff — Mathlib

English

For any action by a group G on V that commutes with k-scalar multiplication, an element p of V lies in a-subset s after scaling by a iff p lies in s.

Русский

Для группы G, действующей на V и согласующейся с умножением на скаляры k, мы имеем условие: a·p ∈ a·s эквивалентно p ∈ s.

LaTeX

$$$ a \\cdot p \\in a \\cdot s \\;\\longleftrightarrow\\; p \\in s $$$

Lean4

theorem smul_mem_smul_iff {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {a : G} :
    a • p ∈ a • s ↔ p ∈ s :=
  smul_mem_smul_set_iff

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