smul_mem_iff — Mathlib

English

If s is a nonzero scalar acting on M, membership in a submodule p is preserved under multiplying by s: s·x ∈ p iff x ∈ p.

Русский

Если s не равно нулю и действует на M, то принадлежность элементa x подпомодулю p сохраняется при умножении на s: s·x ∈ p эквивалентно x ∈ p.

LaTeX

$$$s \\neq 0 \\Rightarrow (s \\cdot x \\in p \\iff x \\in p)$$$

Lean4

theorem smul_mem_iff (s0 : s ≠ 0) : s • x ∈ p ↔ x ∈ p :=
  p.toSubMulAction.smul_mem_iff s0

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