Documentation

Mathlib.Algebra.Divisibility.Prod

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 : G₁ × G₂} {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₁ : G₁} {y₁ : G₁} {x₂ : G₂} {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₂] :
Equations
  • =
theorem pi_dvd_iff {ι : Type u_1} {G : ιType u_4} [(i : ι) → Semigroup (G i)] {x : (i : ι) → G i} {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
  • =