chainTopCoeff_if_one_zero — Mathlib

English

For a crystallographic, reduced, irreducible RootPairing, the bottom chain coefficient equals 1 if the pairingIn equals 0, otherwise it equals 0.

Русский

Для кристаллизационного, редуцированного, неразложимого RootPairing нижний коэффициент цепи равен единице, если pairingIn равен нулю, иначе равен нулю.

LaTeX

$$$ P.chainBotCoeff i j = \text{if } P.pairingIn\mathbb{Z} i j = 0 \text{ then } 1 \text{ else } 0 $$$

Lean4

theorem chainTopCoeff_if_one_zero [P.IsNotG2] (h : P.root i - P.root j ∈ range P.root) :
    P.chainTopCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0 :=
  by
  letI := P.indexNeg
  replace h : P.root i + P.root (-j) ∈ range P.root := by simpa [← sub_eq_add_neg] using h
  simpa using P.chainBotCoeff_if_one_zero h

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