pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'

English

If IsReduced holds, then (P.pairingIn ℤ i j, P.pairingIn ℤ j i) belongs to a small finite set determining crystallographic conditions.

Русский

При выполнении условия IsReduced пара сопряжений принадлежит небольшому конечному множеству, задающему кристаллографические условия.

LaTeX

$$(P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(0,0),(1,1),(-1,-1)} : Set (ℤ × ℤ))$$

Lean4

theorem pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' [P.IsReduced] (hij : α i ≠ α j) (hij' : α i ≠ -α j) :
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
      ({(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)} :
        Set (ℤ × ℤ)) :=
  by
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
  simp_all

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