English
There exists a decomposition of a divisor k of m n into a product of a divisor of m and a divisor of n, under suitable conditions in a nonempty gcd-monoid.
Русский
Существует разложение делителя k делимого m n на произведение делителя m на делитель n в подходящем контексте непустого gcd-монойда.
LaTeX
$$$\\exists m',n' : \\alpha, (m' \\mid m) \\wedge (n' \\mid n) \\wedge k = m' n'$$$
Lean4
/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.
Note: In general, this representation is highly non-unique.
See `Nat.dvdProdDvdOfDvdProd` for a constructive version on `ℕ`. -/
instance [h : Nonempty (GCDMonoid α)] : DecompositionMonoid α where
primal k m n
H := by
cases h
by_cases h0 : gcd k m = 0
· rw [gcd_eq_zero_iff] at h0
rcases h0 with ⟨rfl, rfl⟩
exact ⟨0, n, dvd_refl 0, dvd_refl n, by simp⟩
· obtain ⟨a, ha⟩ := gcd_dvd_left k m
refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
rw [← mul_dvd_mul_iff_left h0, ← ha]
exact dvd_gcd_mul_of_dvd_mul H
