pairingIn_pairingIn_mem_set_of_length_eq_of_ne

English

The Coxeter weight vanishes exactly when the corresponding pairing vanishes: coxeterWeightIn ℤ i j = 0 iff pairingIn ℤ i j = 0.

Русский

Коксетерова масса обращается в ноль тогда и только тогда, когда сопряжение обращается в ноль: coxeterWeightIn ℤ i j = 0 ⇔ pairingIn ℤ i j = 0.

LaTeX

$$P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0$$

Lean4

theorem pairingIn_pairingIn_mem_set_of_length_eq_of_ne {B : P.InvariantForm}
    (len_eq : B.form (α i) (α i) = B.form (α j) (α j)) (ne : i ≠ j) (ne' : α i ≠ -α j) :
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(0, 0), (1, 1), (-1, -1)} : Set (ℤ × ℤ)) :=
  by
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have := P.pairingIn_pairingIn_mem_set_of_length_eq len_eq
  simp_all

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