English
For x,y ∈ G1 × G2 with G1,G2 semigroups, x ∣ y iff x1 ∣ y1 and x2 ∣ y2.
Русский
Для x,y ∈ G1 × G2, где G1,G2 — полугруппы, x делит y тогда и только тогда, когда x1 делит y1 и x2 делит y2.
LaTeX
$$$ x \mid y \iff x.1 \mid y.1 \land x.2 \mid y.2 $$$
Lean4
theorem prod_dvd_iff {x y : G₁ × G₂} : x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2 :=
by
cases x; cases y
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq, exists_and_left, exists_and_right]