mul_eq_mul_prime_pow
theorem mul_eq_mul_prime_pow :
∀ {R : Type u_1} [inst : CancelCommMonoidWithZero R] {x y a p : R} {n : ℕ},
Prime p → x * y = a * p ^ n → ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
The theorem `mul_eq_mul_prime_pow` states that for any type `R` that is a cancellative commutative monoid with zero, given elements `x`, `y`, `a`, and `p` from `R`, and a natural number `n`, if `p` is a prime element and the product of `x` and `y` is equal to the product of `a` and the `n`-th power of `p`, then there exist natural numbers `i` and `j`, and elements `b` and `c` of `R`, such that the sum of `i` and `j` is `n`, `a` is the product of `b` and `c`, `x` is the product of `b` and the `i`-th power of `p`, and `y` is the product of `c` and the `j`-th power of `p`. In other words, both `x` and `y` can be expressed as the product of a power of the prime `p` and a factor of `a`.
More concisely: If `x` and `y` are elements of a cancellative commutative monoid with zero, `p` is a prime element, and `p^n = axy` for some natural number `n`, then there exist natural numbers `i`, `j` and elements `b`, `c` in the monoid such that `i + j = n`, `a = bc`, `x = bp^i`, and `y = cp^j`.
|
mul_eq_mul_prime_prod
theorem mul_eq_mul_prime_prod :
∀ {R : Type u_1} [inst : CancelCommMonoidWithZero R] {α : Type u_2} [inst_1 : DecidableEq α] {x y a : R}
{s : Finset α} {p : α → R},
(∀ i ∈ s, Prime (p i)) →
(x * y = a * s.prod fun i => p i) →
∃ t u b c,
t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ (x = b * t.prod fun i => p i) ∧ y = c * u.prod fun i => p i
This theorem states that if we have an equation `x * y = a * ∏ i in s, p i` in a cancelable commutative monoid with zero (such as a ring without zero divisors), where `p i` is always a prime element and `s` is a finite set of indices, then there exist subsets `t` and `u` of `s` such that `t` and `u` form a partition of `s` (i.e., `t ∪ u = s` and `t` and `u` are disjoint), and elements `b` and `c` such that `a = b * c`, `x` can be written as `b` times the product of `p i` for `i` in `t`, and `y` can be written as `c` times the product of `p i` for `i` in `u`.
This theorem is essentially a generalized form of unique factorization into primes, which states that any element in a unique factorization domain can be written as a product of prime elements (up to order and units).
More concisely: In a commutative monoid with zero and finite index set `s` of prime elements `p i`, any equation `x * y = a * ∏ i in s, p i` admits a partition `t` and `u` of `s` such that `x` is the product of `p i` for `i` in `t`, `y` is the product of `p i` for `i` in `u`, and `a = b * c` with `b` the product of `p i` for `i` in `t` and `c` the product of `p i` for `i` in `u`.
|