English
Let Φ be a crystallographic root system with index set ι and roots α_i. If two roots form an obtuse angle, i.e. ⟨α_i, α_j^∨⟩ < 0, and α_i ≠ −α_j, then α_i + α_j is a root, i.e. α_i + α_j ∈ Φ.
Русский
Пусть Φ — кристаллографическая корневая система с индексами ι и корнями α_i. Если два корня образуют тупой угол, т.е. ⟨α_i, α_j^∨⟩ < 0, и α_i ≠ −α_j, то сумма α_i + α_j является корнем, то есть α_i + α_j ∈ Φ.
LaTeX
$$$\forall i,j\in ι,\ (α_i \neq -α_j) \land \langle α_i, α_j^\vee \rangle < 0 \Rightarrow α_i + α_j \in Φ$$$
Lean4
/-- If two roots make an obtuse angle then their sum is a root (provided it is not zero).
See `RootPairing.pairingIn_le_zero_of_root_add_mem` for a partial converse. -/
theorem root_add_root_mem_of_pairingIn_neg (h : P.pairingIn ℤ i j < 0) (h' : α i ≠ -α j) : α i + α j ∈ Φ :=
by
let _i := P.indexNeg
replace h : 0 < P.pairingIn ℤ i (-j) := by simpa
replace h' : i ≠ -j := by contrapose! h'; simp [h']
simpa using P.root_sub_root_mem_of_pairingIn_pos h h'
