pairingIn_same

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

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

← MathLib Explorer

English

If S-valued, then for every i, pairingIn S i i equals 2.

Русский

Если значения в S, то для каждого i парирование в i равно 2.

LaTeX

$$$P.pairingIn\;S\;i\;i = 2,$$$

Lean4

@[simp]
theorem pairingIn_same [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) : P.pairingIn S i i = 2 :=
  FaithfulSMul.algebraMap_injective S R <| by simp [map_ofNat]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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