prod_dvd_iff — Mathlib

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]

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