English
In a generalized setting with an additive structure, if a,b ∈ α (α has 0,1) satisfy a = 0 ↔ b = 0, then a·b ∈ {0,1,2,3,4} iff (a,b) lies in the corresponding finite set of pairs in α × α (the same 17-pattern translated into α).
Русский
В обобщённой ситуации с добавочной структурой, если a,b ∈ α (где α имеет 0 и 1) удовлетворяют a = 0 ⇔ b = 0, то ab ∈ {0,1,2,3,4} тогда и только тогда, когда (a,b) принадлежит соответствующему конечному множеству пар в α × α (та же 17-паттерн, перенесённый в α).
LaTeX
$$$ a,b \in \alpha \ (\text{with } 0,1),\ (a=0 \iff b=0) \implies a b \in \{0,1,2,3,4\} \iff (a,b) \in \{(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)\}.$$$
Lean4
/-- This lemma justifies its existence from its utility in crystallographic root system theory. -/
theorem mul_mem_zero_one_two_three_four_iff {a b : ℤ} (h₀ : a = 0 ↔ b = 0) :
a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ) ↔
(a, b) ∈
({(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
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq, one_ne_zero,
not_false_eq_true, OfNat.ofNat_ne_zero]
aesop
