flip_flip

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.flip_flip

English

The flip construction preserves all structural properties of the root pairing.

Русский

Перестановка flip сохраняет все структурные свойства пары корней.

LaTeX

$$$$ \text{flip preserves structure} $$$$

Lean4

@[simp]
theorem flip_flip : P.flip.flip = P :=
  rfl

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

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

Разделы

Аффилиация

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