pairingIn_le_zero_of_ne — Mathlib

English

If i ≠ j are indices in the base and in addition to crystallographic and finite assumptions, then the pairing value P.pairingIn ℤ i j is ≤ 0.

Русский

Если i ≠ j, и выполняются условия кристалографичности и конечности, то P.pairingIn ℤ i j ≤ 0.

LaTeX

$$P.pairingIn ℤ i j ≤ 0$$

Lean4

theorem pairingIn_le_zero_of_ne [IsDomain R] [P.IsCrystallographic] [Finite ι] {i j} (hij : i ≠ j) (hi : i ∈ b.support)
    (hj : j ∈ b.support) : P.pairingIn ℤ i j ≤ 0 := by
  by_contra! h
  exact b.sub_notMem_range_root hi hj <| P.root_sub_root_mem_of_pairingIn_pos h hij

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