mem_smul

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.mem_smul

English

An element b belongs to s • t if and only if there exist a ∈ s and c ∈ t with a • c = b.

Русский

Элемент b принадлежит s • t тогда и только тогда, когда существуют a ∈ s и c ∈ t с a • c = b.

LaTeX

$$$$ b \in s \cdot t \iff \exists a \in s, \exists c \in t, a \cdot c = b $$$$

Lean4

@[to_additive]
theorem mem_smul : b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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