smul_mem_pointwise_smul_iff

Mathlib.Algebra.Ring.Subring.Pointwise

URI: https://scilib.ai/kg/mathlib#Subring.smul_mem_pointwise_smul_iff

English

For all a ∈ M, S ⊆ R, x ∈ R, a•x ∈ a•S iff x ∈ S.

Русский

Для всех a ∈ M, S ⊆ R, x ∈ R: a•x ∈ a•S эквивалентно x ∈ S.

LaTeX

$$$a \cdot x \in a \cdot S \iff x \in S$$$

Lean4

@[simp]
theorem smul_mem_pointwise_smul_iff {a : M} {S : Subring R} {x : R} : a • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru