pairing_eq_zero_of_add_notMem_of_sub_notMem

English

If i ≠ j, α_i ≠ −α_j and α_i + α_j ∉ Φ, α_i − α_j ∉ Φ, then the root pairing P.pairing i j equals 0.

Русский

Если i ≠ j, α_i ≠ −α_j и α_i + α_j ∉ Φ, α_i − α_j ∉ Φ, то P.pairing 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.pairing i j = 0$$$

Lean4

theorem pairing_eq_zero_of_add_notMem_of_sub_notMem (hp : i ≠ j) (hn : α i ≠ -α j) (h_add : α i + α j ∉ Φ)
    (h_sub : α i - α j ∉ Φ) : P.pairing i j = 0 := by
  rw [← P.algebraMap_pairingIn ℤ, P.pairingIn_eq_zero_of_add_notMem_of_sub_notMem hp hn h_add h_sub, map_zero]

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