smul_mem_pointwise_smul_iff

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

The same as 13474, but without assumption ha ≠ 0.

Русский

То же самое, что и в 13474, без предположения ha ≠ 0.

LaTeX

$$$ (a \\cdot S).toAddSubmonoid = a \\cdot S.toAddSubmonoid $$$

Lean4

@[simp]
theorem smul_mem_pointwise_smul_iff : a • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff

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

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

Разделы

Аффилиация

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