pow_swap

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.pow_swap

English

Exponentiation commutes with swapping coordinates: (p^c).swap = p.swap^c.

Русский

Возведение в степень коммутирует со сменой координат: (p^c).swap = p.swap^c.

LaTeX

$$$ (p^c).swap = p.swap^c $$$

Lean4

@[to_additive existing (attr := simp) (reorder := 6 7) smul_swap]
theorem pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c :=
  rfl

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

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

Разделы

Аффилиация

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