English
For i,j, if B.form(α_i, α_i) and B.form(α_j, α_j) are related by one of a finite set of multiples, then a similar finite set of relations holds for the swapped roles; i.e., there is a symmetric 5-way relation between B(α_i, α_i) and B(α_j, α_j).
Русский
Для любых i,j существует конечное множество отношений между B(α_i, α_i) и B(α_j, α_j), сохраняющее симметрию при обмене индексов.
LaTeX
$$см. формула из apply_eq_or, с учётом выбора j' и эквивалентной симметрии$$
Lean4
/-- Relative of lengths of roots in a reduced irreducible finite crystallographic root pairing are
very constrained. -/
theorem apply_eq_or (i j : ι) :
B.form (α i) (α i) = B.form (α j) (α j) ∨
B.form (α i) (α i) = 2 * B.form (α j) (α j) ∨
B.form (α i) (α i) = 3 * B.form (α j) (α j) ∨
B.form (α j) (α j) = 2 * B.form (α i) (α i) ∨ B.form (α j) (α j) = 3 * B.form (α i) (α i) :=
by
obtain ⟨j', h₁, h₂⟩ := P.exists_form_eq_form_and_form_ne_zero B i j
suffices P.pairingIn ℤ i j' ≠ 0 by simp only [← h₁, B.apply_eq_or_aux i j' this]
contrapose! h₂
replace h₂ : P.pairing i j' = 0 := by rw [← P.algebraMap_pairingIn ℤ, h₂, map_zero]
exact (B.apply_root_root_zero_iff i j').mpr h₂
