pairingIn_pairingIn_mem_set_of_length_eq

English

Same content as item 133819; membership of a length-equality induced set.

Русский

То же содержимое, что и в пункте 133819; принадлежность пары к ограниченному множеству.

LaTeX

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

Lean4

theorem pairingIn_pairingIn_mem_set_of_length_eq {B : P.InvariantForm}
    (len_eq : B.form (α i) (α i) = B.form (α j) (α j)) :
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} : Set (ℤ × ℤ)) :=
  by
  replace len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i :=
    by
    simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]
    exact mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap j i)
  have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
  aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)

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