smul_finset_singleton

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

The singleton-smul lemma: a • {b} = {a • b}.

Русский

Лемма одиночного умножения: a • {b} = {a • b}.

LaTeX

$$$a \cdot \{b\} = \{a \cdot b\}$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_finset_singleton (b : β) : a • ({ b } : Finset β) = {a • b} :=
  image_singleton ..

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

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

Разделы

Аффилиация

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