instIsValuedIn

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

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

English

If P is valued in S, then the flip P.flip is valued in S as well.

Русский

Если P имеет значение в S, то и P.flip имеет значение в S.

LaTeX

$$$$ \text{If } P.IsValuedIn S, \text{ then } P.flip.IsValuedIn S. $$$$

Lean4

instance : P.IsValuedIn R where exists_value i j := by simp

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

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

Разделы

Аффилиация

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