exists_dvd_and_dvd_of_dvd_mul — Mathlib

English

If a divides b·c in a DecompositionMonoid, there exist a1,a2 such that a1|b, a2|c and a=a1·a2.

Русский

Если a делит b·c в декомпозиционном моноиде, существуют a1,a2 такие, что a1|b, a2|c и a=a1·a2.

LaTeX

$$$$\exists a_1,a_2:\ semigroupDvd.dvd a_1 b \land \semigroupDvd.dvd a_2 c \land a = a_1 a_2.$$$$

Lean4

theorem exists_dvd_and_dvd_of_dvd_mul [DecompositionMonoid α] {b c a : α} (H : a ∣ b * c) :
    ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂ :=
  DecompositionMonoid.primal a H

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