mem_pointwise_smul_iff_inv_smul_mem₀

English

Let a be a nonzero acting element and S an additive submonoid of A. An element x lies in a · S precisely when a⁻¹ · x lies in S.

Русский

Пусть a не равно нулю и S — аддитивный подмоноид A. Элемент x принадлежит a · S тогда и только тогда, когда a⁻¹ · x принадлежит S.

LaTeX

$$$\forall a\neq 0,\ S:\text{AddSubmonoid } A,\ \forall x\in A:\ x \in a\cdot S\iff a^{-1}\cdot x \in S.$$$

Lean4

theorem mem_pointwise_smul_iff_inv_smul_mem₀ (ha : a ≠ 0) (S : AddSubmonoid A) (x : A) : x ∈ a • S ↔ a⁻¹ • x ∈ S :=
  mem_smul_set_iff_inv_smul_mem₀ ha (S : Set A) x

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