English
If α i ≠ α j and α i ≠ −α j and P.pairingIn ℤ i j ∉ {−1,0,1}, then B.rootLength j < B.rootLength i for B a RootPositiveForm.
Русский
Если α i ≠ α j и α i ≠ −α j, и P.pairingIn ℤ i j ∉ {−1,0,1}, тогда B.rootLength j < B.rootLength i.
LaTeX
$$B.rootLength i ≤ B.rootLength j → False$$
Lean4
theorem rootLength_le_of_pairingIn_eq (B : P.RootPositiveForm ℤ) {i j : ι}
(hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1) : B.rootLength i ≤ B.rootLength j :=
by
have h :
(P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
({(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)} : Set (ℤ × ℤ)) :=
by
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at h
have h' := B.pairingIn_mul_eq_pairingIn_mul_swap i j
have hi := B.rootLength_pos i
rcases h with hij' | hij' | hij' | hij' | hij' | hij' | hij' | hij' <;> rw [hij'.1, hij'.2] at h' <;> omega
