smul_mem_pointwise_smul_iff₀

Mathlib.Algebra.GroupWithZero.Subgroup

URI: https://scilib.ai/kg/mathlib#AddSubgroup.smul_mem_pointwise_smul_iff₀

← MathLib Explorer

English

For ha ≠ 0, a • x ∈ a • S ↔ x ∈ S.

Русский

Для ha ≠ 0: a • x ∈ a • S ↔ x ∈ S.

LaTeX

$$$ (ha \\neq 0) \\Rightarrow a \\cdot x \\in a \\cdot S \\iff x \\in S $$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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