English
In a cancellative commutative monoid with zero, if x y = a p^{n} with p prime, then there exist i,j ∈ ℕ and b,c ∈ R such that i + j = n, a = b c, x = b p^{i}, y = c p^{j}.
Русский
В_CANCEL-коммутативном моноиде с нулём, если x y = a p^{n} при простом p, то существуют i,j ∈ ℕ и b,c ∈ R такие, что i+j=n, a=bc, x=b p^{i}, y=c p^{j}.
LaTeX
$$$\text{Prime}(p)\ \land\ x y = a p^{n} \Rightarrow \exists i,j,b,c\in R,\ i+j=n \land a=bc \land x=b p^{i} \land y=c p^{j}$$$
Lean4
/-- If `x * y = a * p ^ n` where `p` is prime, then `x` and `y` can both be written
as the product of a power of `p` and a divisor of `a`. -/
theorem mul_eq_mul_prime_pow {x y a p : R} {n : ℕ} (hp : Prime p) (hx : x * y = a * p ^ n) :
∃ (i j : ℕ) (b c : R), i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j :=
by
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp) (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
exact ⟨#t, #u, b, c, by rw [← card_union_of_disjoint htu, htus, card_range], by simp⟩
