smul_finset_sdiff

Mathlib.Algebra.Group.Action.Pointwise.Finset

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

English

The smul distributes over set difference: a • (s \\ t) = a • s \\ a • t.

Русский

Перенос через разность: a • (s \\ t) = a • s \\ a • t.

LaTeX

$$$a \\cdot (s \\setminus t) = (a \\cdot s) \\setminus (a \\cdot t)$$$

Lean4

@[to_additive]
theorem smul_finset_sdiff : a • (s \ t) = a • s \ a • t :=
  image_sdiff _ _ <| MulAction.injective a

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

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

Разделы

Аффилиация

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