Lemmas about the divisibility relation in product (semi)groups

theorem prod_dvd_iff {G₁ : Type u_2} {G₂ : Type u_3} [Semigroup G₁] [Semigroup G₂] {x y : G₁ × G₂} : x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

@[simp]

theorem Prod.mk_dvd_mk {G₁ : Type u_2} {G₂ : Type u_3} [Semigroup G₁] [Semigroup G₂] {x₁ y₁ : G₁} {x₂ y₂ : G₂} : (x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂

instance instDecompositionMonoidProd {G₁ : Type u_2} {G₂ : Type u_3} [Semigroup G₁] [Semigroup G₂] [DecompositionMonoid G₁] [DecompositionMonoid G₂] : DecompositionMonoid (G₁ × G₂)

Equations

• ⋯ = ⋯

theorem pi_dvd_iff {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Semigroup (G i)] {x y : (i : ι) → G i} : x ∣ y ↔ ∀ (i : ι), x i ∣ y i

instance instDecompositionMonoidForall {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Semigroup (G i)] [∀ (i : ι), DecompositionMonoid (G i)] : DecompositionMonoid ((i : ι) → G i)

Equations

• ⋯ = ⋯