smul_finset_symmDiff

Mathlib.Algebra.Group.Action.Pointwise.Finset

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

English

The smul distributes over symmetric difference: a • (s Δ t) = (a • s) Δ (a • t).

Русский

Перенос через симметрическую разность: a • (s Δ t) = (a • s) Δ (a • t).

LaTeX

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

Lean4

@[to_additive]
theorem smul_finset_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
  image_symmDiff _ _ <| MulAction.injective a

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

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

Разделы

Аффилиация

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