mk_dvd_mk — Mathlib

English

The divisibility of a pair in a product is equivalent to the pairwise divisibilities of components.

Русский

Делимость пары в произведении эквивалентна попарной делимости компонент.

LaTeX

$$$ (x1, x2) \mid (y1, y2) \iff (x1 \mid y1) \land (x2 \mid y2) $$$

Lean4

@[simp]
theorem mk_dvd_mk {x₁ y₁ : G₁} {x₂ y₂ : G₂} : (x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂ :=
  prod_dvd_iff

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