sym_symm

Mathlib.Algebra.Symmetrized

URI: https://scilib.ai/kg/mathlib#SymAlg.sym_symm

English

The inverse of sym is unsym, i.e., sym^(-1) = unsym.

Русский

Обратное отображение к sym равно unsym: sym^{-1} = unsym.

LaTeX

$$$\mathrm{sym}^{-1} = \mathrm{unsym}$$$

Lean4

@[simp]
theorem sym_symm : (@sym α).symm = unsym :=
  rfl

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

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

Разделы

Аффилиация

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