pairingIn_le_zero_iff — Mathlib

English

A crystallographic, reduced, irreducible RootPairing P has IsG2 if and only if there exist indices i and j with pairingInℤ i j = −3.

Русский

Кристаллографическое, редуцируемое и неразложимое корневое соответствие имеет свойство IsG2 тогда и только тогда, когда существуют индексы i, j такие, что pairingInℤ i j = −3.

LaTeX

$$$ P.IsG2 \iff \exists i,j, \ P.pairingIn\mathbb{Z} i j = -3 $$$

Lean4

theorem pairingIn_le_zero_iff [NeZero (2 : R)] [NoZeroSMulDivisors R M] :
    P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0 :=
  by
  rcases eq_or_ne (P.pairingIn S i j) 0 with hij | hij <;> rcases eq_or_ne (P.pairingIn S j i) 0 with hji | hji
  · rw [hij, hji]
  · rw [hij, P.pairingIn_eq_zero_iff.mp hij]
  · rw [hji, P.pairingIn_eq_zero_iff.mp hji]
  · rw [le_iff_eq_or_lt, le_iff_eq_or_lt, or_iff_right hij, or_iff_right hji]
    exact P.pairingIn_lt_zero_iff S

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