coxeterWeightIn_eq_zero_iff — Mathlib

English

Equivalent to item 133821; equality of zero-ness between Coxeter weight and pairing.

Русский

Эквивалентно пункту 133821, нулевость массы и сопряжения совпадают.

LaTeX

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

Lean4

theorem coxeterWeightIn_eq_zero_iff : P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [coxeterWeightIn, h, zero_mul]⟩
  rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal, P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ←
    P.algebraMap_pairingIn ℤ, FaithfulSMul.algebraMap_eq_zero_iff] at h

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