mul_mem_smul_finset_iff

Mathlib.Algebra.Group.Action.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.mul_mem_smul_finset_iff

← MathLib Explorer

English

For any a ∈ α, a*b ∈ a•s iff b ∈ s, in the multiplicative setting.

Русский

Для любого a ∈ α: a*b ∈ a•s тогда и только если b ∈ s.

LaTeX

$$$a \\cdot b \\in a \\cdot s \\iff b \\in s$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_mem_smul_finset_iff [DecidableEq α] (a : α) {b : α} {s : Finset α} : a * b ∈ a • s ↔ b ∈ s :=
  smul_mem_smul_finset_iff _

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

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

Разделы

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

Аффилиация

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