pairing_eq_add_of_root_eq_add — Mathlib

English

If root k equals root i plus root j, then the pairing with any fixed l is additive: pairing(k,l) = pairing(i,l) + pairing(j,l).

Русский

Если корень k равен корню i плюс корень j, тогда парирование с фиксированным l суммируется: pairing(k,l) = pairing(i,l) + pairing(j,l).

LaTeX

$$$ \text{If } P.root(k) = P.root(i) + P.root(j), \; P.pairing(k,l) = P.pairing(i,l) + P.pairing(j,l) $$$

Lean4

theorem pairing_eq_add_of_root_eq_add {i j k l : ι} (h : P.root k = P.root i + P.root j) :
    P.pairing k l = P.pairing i l + P.pairing j l := by
  simp only [← root_coroot_eq_pairing, h, map_add, LinearMap.add_apply]

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