mem_smul_pointwise_iff_exists

Mathlib.Algebra.GroupWithZero.Subgroup

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

← MathLib Explorer

English

x ∈ a • S iff there exists s ∈ S with a • s = x.

Русский

x ∈ a • S эквивалентно существованию s ∈ S такого, что a • s = x.

LaTeX

$$$ x \\in a \\cdot S \\iff \\exists s \\in S, a \\cdot s = x $$$

Lean4

theorem mem_smul_pointwise_iff_exists (m : A) (a : M) (S : AddSubgroup A) : m ∈ a • S ↔ ∃ s : A, s ∈ S ∧ a • s = m :=
  (Set.mem_smul_set : m ∈ a • (S : Set A) ↔ _)

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

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

Разделы

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

Аффилиация

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