Theorems · Theorem · commutative algebra

mul_eq_mul_prime_prod

∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {α : Type u_2} [inst_2 : DecidableEq α] {x y a : R}
  {s : Finset α} {p : α → R},
  (∀ i ∈ s, Prime (p i)) →
    x * y = a * ∏ i ∈ s, p i →
      ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

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

Defined in

Mathlib.RingTheory.Prime

Cited by

1 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroIsCancelMulZeroDecidableEq