pairingIn_pairingIn_mem_set_of_isCrystallographic

English

Same as item 133814: membership in {0,1,2,3,4} for crystallographic P.

Русский

То же, что и в пункте 133814: принадлежность к {0,1,2,3,4} для кристаллографичного P.

LaTeX

$$P.coxeterWeightIn ℤ i j ∈ \{0,1,2,3,4\}$$

Lean4

theorem pairingIn_pairingIn_mem_set_of_isCrystallographic :
    (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), (4, 1),
          (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} :
        Set (ℤ × ℤ)) :=
  by
  refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)
  simpa [← P.algebraMap_pairingIn ℤ] using P.pairing_eq_zero_iff' (i := i) (j := j)

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