mk_prod_swap_eq

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.mk_prod_swap_eq

English

Sym2.mk(p.swap) = Sym2.mk(p) for any p ∈ α×α.

Русский

Для любого p ∈ α×α выполняется Sym2.mk(p.swap) = Sym2.mk(p).

LaTeX

$$$$ \ Sym2.mk p.swap = \ Sym2.mk p. $$$$

Lean4

@[simp]
theorem mk_prod_swap_eq {p : α × α} : Sym2.mk p.swap = Sym2.mk p :=
  by
  cases p
  exact eq_swap

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

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

Разделы

Аффилиация

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