smul_swap

Mathlib.Algebra.Group.Action.Sum

URI: https://scilib.ai/kg/mathlib#Sum.smul_swap

English

The smul operation on Sum is compatible with swapping components: (a • x).swap = a • x.swap.

Русский

Операция smul на Sum совместима с перестановкой компонентов: (a • x).swap = a • x.swap.

LaTeX

$$$ (a \cdot x).\text{swap} = a \cdot x.\text{swap}. $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_swap : (a • x).swap = a • x.swap := by cases x <;> rfl

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

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

Разделы

Аффилиация

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