toPerfPair_comp_root

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The composition of the perf-pair with root satisfies a compatibility relation: P.toPerfPair ∘ P.root = P.root'.

Русский

Существование совместимости между оболочкой perf-пары и корнем: P.toPerfPair ∘ P.root = P.root'.

LaTeX

$$$$ P.toPerfPair \\circ P.root = P.root'. $$$$

Lean4

@[simp]
theorem toPerfPair_comp_root : P.toPerfPair ∘ P.root = P.root' :=
  rfl

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

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

Разделы

Аффилиация

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