pairingIn_eq_zero_of_add_notMem_of_sub_notMem

English

Let i,j ∈ ι with i ≠ j and α_i ≠ −α_j. If neither α_i + α_j nor α_i − α_j belongs to Φ, then the root pairing in integers vanishes: P.pairingIn ℤ i j = 0.

Русский

Пусть i, j ∈ ι с i ≠ j и α_i ≠ −α_j. Если ни α_i + α_j, ни α_i − α_j не принадлежит Φ, то пары корней в целых нуля: P.pairingIn ℤ i j = 0.

LaTeX

$$$\forall i,j\in ι,\ (i \neq j) \land (α_i \neq -α_j) \land (α_i + α_j \notin Φ) \land (α_i - α_j \notin Φ) \Rightarrow P.pairingIn \mathbb{Z} \ i \ j = 0$$$

Lean4

theorem pairingIn_eq_zero_of_add_notMem_of_sub_notMem (hp : i ≠ j) (hn : α i ≠ -α j) (h_add : α i + α j ∉ Φ)
    (h_sub : α i - α j ∉ Φ) : P.pairingIn ℤ i j = 0 :=
  by
  apply le_antisymm
  · contrapose! h_sub
    exact root_sub_root_mem_of_pairingIn_pos P h_sub hp
  · contrapose! h_add
    exact root_add_root_mem_of_pairingIn_neg P h_add hn

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