mem_inv_pointwise_smul_iff — Mathlib

English

Let a ∈ M and S ⊆ R be a subring. For every x ∈ R, x ∈ a^{-1} · S if and only if a · x ∈ S.

Русский

Пусть a ∈ M и S — подкольцо R. Тогда для любого x ∈ R верно: x ∈ a^{-1} · S ⇔ a · x ∈ S.

LaTeX

$$$\forall a \in M, S \subseteq R:\ x \in a^{-1} \cdot S \iff a \cdot x \in S$$$

Lean4

theorem mem_inv_pointwise_smul_iff {a : M} {S : Subring R} {x : R} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
  mem_inv_smul_set_iff

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