singleton_smul

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

{a} • t = a • t.

Русский

{a} • t = a • t.

LaTeX

$$$$ \{ a \} \cdot t = a \cdot t $$$$

Lean4

@[to_additive (attr := simp low + 1)]
theorem singleton_smul : ({ a } : Set α) • t = a • t :=
  image2_singleton_left

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

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

Разделы

Аффилиация

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