smul_mem_pointwise_smul_iff₀ — Mathlib

English

For a nonzero a and Submonoid S of M, a • x ∈ a • S iff ∃ s ∈ S, m • s = a.

Русский

При ненулевом a и подмономе S подмножество M, a • x ∈ a • S тогда и только если существует s ∈ S такое, что m • s = a.

LaTeX

$$$ (a \neq 0) \Rightarrow (a \cdot x \in a \cdot S \iff \exists s \in S,\; m \cdot s = a) $$$

Lean4

@[simp]
theorem smul_mem_pointwise_smul_iff₀ (ha : a ≠ 0) (S : Submonoid M) (x : M) : a • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff₀ ha (S : Set M) x

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