English
This restates span_eq_rootSpan_int with G2-structure: for i,j as in the base, the same span equality holds over integers.
Русский
Это повтор espansия span_eq_rootSpan_int в структуре G2: для i, j в базисе та же равенство обобщённой оболочки над ℤ сохраняется.
LaTeX
$$Eq (Submodule.span ℤ {P.root i, P.root j}) (P.rootSpan ℤ)$$
Lean4
theorem pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed [P.IsReduced] :
(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), (2, 2),
(-2, -2)} :
Set (ℤ × ℤ)) :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
rcases eq_or_ne i j with rfl | h₁; · simp
rcases eq_or_ne (α i) (-α j) with h₂ | h₂; · simp_all
have aux₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
have aux₂ : P.pairingIn ℤ i j * P.pairingIn ℤ j i ≠ 4 := P.coxeterWeightIn_ne_four ℤ h₁ h₂
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
