mul_eq_mul_prime_prod — Mathlib

English

In a cancellative commutative monoid with zero, if x y = a ∏_{i∈s} p(i) where each p(i) is prime, then x and y can be written as x = b ∏_{i∈t} p(i) and y = c ∏_{i∈u} p(i) for some disjoint subsets t,u with t ∪ u = s and a = b c.

Русский

В коммутативном моноиде с нулём, допускающем ◊ отмену, если x y = a ∏_{i∈s} p(i) и каждый p(i) прост, то существуют непересекающиеся подмножества t, u такие, что t ∪ u = s и a = bc, x = b ∏_{i∈t} p(i), y = c ∏_{i∈u} p(i).

LaTeX

$$$\exists t,u: Finset\alpha, b,c\in R\; (t\cup u = s) \land Disjoint t u \land a = b c \land x = b \prod_{i\in t} p(i) \land y = c \prod_{i\in u} p(i)$$$

Lean4

/-- If `x * y = a * ∏ i ∈ s, p i` where `p i` is always prime, then
`x` and `y` can both be written as a divisor of `a` multiplied by
a product over a subset of `s` -/
theorem mul_eq_mul_prime_prod {α : Type*} [DecidableEq α] {x y a : R} {s : Finset α} {p : α → R}
    (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i) :
    ∃ (t u : Finset α) (b c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ (x = b * ∏ i ∈ t, p i) ∧ y = c * ∏ i ∈ u, p i :=
  by
  induction s using Finset.induction generalizing x y a with
  | empty => exact ⟨∅, ∅, x, y, by simp [hx]⟩
  | insert i s his ih =>
    rw [prod_insert his, ← mul_assoc] at hx
    have hpi : Prime (p i) := hp i (mem_insert_self _ _)
    rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
    have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
    have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
    obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
    · rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact
        ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
    · rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
      exact
        ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩

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