pairingIn_eq_add_of_root_eq_add — Mathlib

English

If P.root k = P.root i + P.root l, then the corresponding pairings satisfy P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j for all j.

Русский

Если корень k равен сумме корней i и l, тогда соответствующие коэффициенты удовлетворяют P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j для всех j.

LaTeX

$$$P.root\;k = P.root\;i + P.root\;l \;\Rightarrow\; P.pairingIn\;S\;k\;j = P.pairingIn\;S\;i\;j + P.pairingIn\;S\;l\;j$$$

Lean4

theorem pairingIn_eq_add_of_root_eq_add [FaithfulSMul S R] [P.IsValuedIn S] {i j k l : ι}
    (h : P.root k = P.root i + P.root l) : P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j :=
  by
  apply FaithfulSMul.algebraMap_injective S R
  simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using pairing_eq_add_of_root_eq_add h

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