UniqueFactorizationMonoid.count_normalizedFactors_eq'
theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R]
[inst_2 : NormalizationMonoid R] [inst_3 : DecidableEq R] {p x : R},
p = 0 ∨ Irreducible p →
normalize p = p →
∀ {n : ℕ},
p ^ n ∣ x → ¬p ^ (n + 1) ∣ x → Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
The theorem `UniqueFactorizationMonoid.count_normalizedFactors_eq'` states that for any mathematical structure `R` that is a cancel commutative monoid with zero, a unique factorization monoid, normalization monoid, and has decidable equality, and any elements `p` and `x` of `R`, if `p` is either 0 or irreducible, and `p` is normalized, then for any natural number `n`, if `p` to the power of `n` divides `x` but `p` to the power of `n+1` does not divide `x`, then the number of times `p` appears in the multiset of normalized factors of `x` is `n`.
In simpler terms, it means that the number of times a normalized prime factor `p` appears in the prime factorization of `x` is the highest power of `p` that divides `x`.
More concisely: For any cancel commutative monoid with zero, unique factorization, normalization, and decidable equality `R`, if `p` is an irreducible and normalized element of `R` that divides `x` but not `x^(1+n)`, then the multiplicity of `p` in the prime factorization of `x` is equal to the smallest integer `n` such that `p^(n+1)` does not divide `x`.
|
UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a p : α}, p ∈ UniqueFactorizationMonoid.normalizedFactors a → p ∣ a
The theorem `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` states that for any type `α` that has instances of `CancelCommMonoidWithZero`, `NormalizationMonoid`, and `UniqueFactorizationMonoid`, if element `p` is in the multiset of normalized factors of `a` (i.e., `p` is a normalized prime factor of `a`), then `p` divides `a`. In other words, every normalized prime factor of a number divides that number.
More concisely: For any type `α` with instances of `CancelCommMonoidWithZero`, `NormalizationMonoid`, and `UniqueFactorizationMonoid`, every normalized prime factor `p` of an element `a` is a divisor of `a`.
|
Associates.factors_0
theorem Associates.factors_0 :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α],
Associates.factors 0 = ⊤
The theorem `Associates.factors_0` states that for any type `α` that is equipped with the structure of a `CancelCommMonoidWithZero` and a `UniqueFactorizationMonoid`, the multiset of irreducible factors (i.e., the `Associates.FactorSet`) of the zero element in `Associates α` is equal to the top element (`⊤`). This can be interpreted as saying that the zero element has an infinite number of irreducible factors.
More concisely: For any `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid` type `α`, the irreducible factors of its zero element form an infinite set equal to the top element in the `Associates.FactorSet`.
|
UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors
theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] {a b c : R},
a ≠ 0 → (∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ b
The theorem, known as Euclid's lemma, states that in a unique factorization monoid with zero (a structure similar to a ring but with unique factorization of elements), for any non-zero elements `a`, `b`, and `c`, if `a` divides the product of `b` and `c`, and there are no common prime factors between `a` and `c`, then `a` must divide `b`. In more mathematical terms, if $a \neq 0$ and there are no prime numbers $d$ such that $d$ divides both $a$ and $c$, and if $a$ divides $b \times c$, then $a$ divides $b$. This theorem is a generalized version of Euclid's lemma, which is a basic result in Number Theory.
More concisely: If $a$ is a non-zero element in a unique factorization monoid with zero, and there are no prime factors common to $a$ and $c$, then $a$ divides $b$ given that $a$ divides their product $b \times c$.
|
prime_factors_irreducible
theorem prime_factors_irreducible :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a : α} {f : Multiset α},
Irreducible a → (∀ b ∈ f, Prime b) ∧ Associated f.prod a → ∃ p, Associated a p ∧ f = {p}
This theorem states that for any type `α` that is a cancellative commutative monoid with zero, given an element `a` of this type and a multiset `f` of elements of the same type, if `a` is irreducible and all elements of `f` are prime and the product of the elements of `f` is associated with `a`, then there exists a prime element `p` such that `a` is associated with `p` and `f` is a multiset containing only `p`. Essentially, it says that if an irreducible element has a prime factorization, then it must be an associate of one of its prime factors.
More concisely: For any cancellative commutative monoid with zero containing an irreducible element `a` and a multiset `f` of prime elements whose product is associated with `a`, there exists a prime element `p` such that `a` is an associate of `p` and `f` is the multiset containing only `p`.
|
UniqueFactorizationMonoid.ne_zero_of_mem_factors
theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {p a : α},
p ∈ UniqueFactorizationMonoid.factors a → a ≠ 0
The theorem `UniqueFactorizationMonoid.ne_zero_of_mem_factors` states that for any type `α` that has a structure of a cancel commutative monoid with zero and a unique factorization monoid, if an element `p` of `α` is in the multiset of prime factors of another element `a` of `α` (using the function `UniqueFactorizationMonoid.factors`), then `a` must not be zero.
More concisely: If `p` is a factor of non-zero `a` in a cancel commutative monoid equipped with unique factorization and zero, then `p` appears in the prime factorization of `a`.
|
Associates.factors_prod
theorem Associates.factors_prod :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : Associates α),
a.factors.prod = a
The theorem `Associates.factors_prod` states that for any type `α` that is a `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid`, and for any element `a` of the associated type `Associates α`, the product of the `FactorSet` of `a` (which is a multiset of its irreducible factors) is equal to `a` itself. In other words, it says that every element of `Associates α` can be represented as a product of its irreducible factors, which aligns with the fundamental theorem of arithmetic.
More concisely: For any `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid` type `α` and its associated `a`, the product of `a`'s irreducible factors in its `FactorSet` equals `a`.
|
UniqueFactorizationMonoid.induction_on_prime_power
theorem UniqueFactorizationMonoid.induction_on_prime_power :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {P : α → Prop}
(s : Finset α) (i : α → ℕ),
(∀ p ∈ s, Prime p) →
(∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) →
(∀ {x : α}, IsUnit x → P x) →
(∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) →
(∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) → P (s.prod fun p => p ^ i p)
This theorem is about a property `P` holding on a product of powers of distinct primes in a unique factorization monoid. It states that if `P` holds for all units and all powers of prime numbers, and if `P` holds for `x` and `y` that are relatively prime then `P` also holds for their product, then `P` will hold for a product of powers of distinct primes. More precisely, given a finite set `s` of elements in a unique factorization monoid where every element is prime and distinct, and a function `i` from elements of `s` to natural numbers, if `P` holds for units and for each element of `s` raised to its corresponding power given by `i`, and also if whenever `x` and `y` are relatively prime with `P` holding for both `x` and `y`, then `P` also holds for `x * y`, then `P` will hold for the product of each element in `s` raised to its power given by `i`.
More concisely: If `P` is a property that holds for units and distinct prime powers in a unique factorization monoid, and `P` holds for relatively prime elements `x` and `y` and their corresponding prime powers, then `P` holds for the product of any distinct prime powers specified by a function `i` from the set of primes.
|
Associates.le_of_count_ne_zero
theorem Associates.le_of_count_ne_zero :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
[inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)]
{m p : Associates α}, m ≠ 0 → Irreducible p → p.count m.factors ≠ 0 → p ≤ m
This theorem, `Associates.le_of_count_ne_zero`, states that for all monoids `α` with a zero element and for all elements `m` and `p` in the set of associates of `α` (`Associates α`), if `m` is not equal to zero, `p` is irreducible, and the count of `p` in the factor set of `m` is not zero, then `p` is less than or equal to `m`. The factor set of `m` is a multiset of irreducible associates.
In other words, in the context of an integral domain (a commutative ring with cancellation and without zero divisors) with unique factorization, an irreducible element `p` that factors into a nonzero element `m` (i.e., `p` is a part of the prime factorization of `m`) is always less than or equal to `m`.
More concisely: In an integral domain with unique factorization, if an irreducible element `p` is a factor of a nonzero element `m`, then `p` is less than or equal to `m`.
|
UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors
theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R]
[inst_2 : NormalizationMonoid R] [inst_3 : DecidableRel Dvd.dvd] [inst_4 : DecidableEq R] {a b : R},
Irreducible a →
b ≠ 0 → multiplicity a b = ↑(Multiset.count (normalize a) (UniqueFactorizationMonoid.normalizedFactors b))
The theorem `UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors` states that for any irreducible element `a` and nonzero element `b` in a unique factorization monoid `R` that also has a normalization monoid structure, the multiplicity of `a` in `b` is exactly the number of times `a`, after normalization, appears in the multiset of normalized factors of `b`. This is under conditions that the divisibility relation in `R` and equality in `R` are decidable. In other words, the number of times a prime factor divides a number is equal to the number of times it appears in the number's prime factorization, after normalization of the factors.
More concisely: For any irreducible element `a` and nonzero element `b` in a unique factorization monoid `R` with a normalization monoid structure and decidable divisibility and equality relations, the multiplicity of `a` in `b` equals the number of occurrences of the normalized form of `a` in the multiset of normalized factors of `b`.
|
UniqueFactorizationMonoid.prime_of_factor
theorem UniqueFactorizationMonoid.prime_of_factor :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
∀ x ∈ UniqueFactorizationMonoid.factors a, Prime x
The theorem `UniqueFactorizationMonoid.prime_of_factor` states that for any type `α` that forms a cancellation commutative monoid with zero and has unique factorization, every element `x` that is a factor (as determined by `UniqueFactorizationMonoid.factors`) of a given element `a` of `α`, is a prime element. Here, a prime element `p` is defined as an element that is not zero, is not a unit, and has the property that if it divides the product of two elements `a` and `b`, then it must divide either `a` or `b`.
More concisely: If `α` is a cancellation commutative monoid with zero and unique factorization, then every non-zero, non-unit factor `x` of an element `a` in `α` is a prime element.
|
UniqueFactorizationMonoid.normalizedFactors_pow
theorem UniqueFactorizationMonoid.normalizedFactors_pow :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {x : α} (n : ℕ),
UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x
This theorem states that for any type `α` that has the structure of a cancel commutative monoid with zero, a normalization monoid, and a unique factorization monoid, and for any element `x` of type `α`, the multiset of normalized prime factors of `x` raised to the power of `n` (where `n` is a natural number) is equal to `n` times the multiset of normalized prime factors of `x`. In mathematical terms, this means that the prime factorization of `x^n` is simply the prime factorization of `x`, repeated `n` times.
More concisely: For any element `x` of a type `α` with the structure of a cancel commutative monoid with zero, a normalization monoid, and a unique factorization monoid, the multiset of normalized prime factors of `x^n` is equal to the `n`-fold repetition of the multiset of normalized prime factors of `x`.
|
UniqueFactorizationMonoid.count_normalizedFactors_eq
theorem UniqueFactorizationMonoid.count_normalizedFactors_eq :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R]
[inst_2 : NormalizationMonoid R] [inst_3 : DecidableEq R] {p x : R},
Irreducible p →
normalize p = p →
∀ {n : ℕ},
p ^ n ∣ x → ¬p ^ (n + 1) ∣ x → Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
This theorem states that for any irreducible factor 'p' of a value 'x' in an integral domain with unique factorization (where the domain is R, a cancel commutative monoid with zero), given that 'p' is its own normalization, the number of times 'p' appears in the multiset of normalized factors of 'x' is determined by the number of times 'p' divides 'x'. In other words, if 'p' to the power of 'n' divides 'x' but 'p' to the power of 'n+1' does not, then 'p' appears 'n' times in the multiset of normalized factors of 'x'. Note that the theorem also assumes that equality in 'R' is decidable.
More concisely: In an integral domain with unique factorization and decidable equality, the number of times an irreducible factor 'p' appears in the multiset of its normalized factors of a value 'x' equals the multiplicity of 'p' as a divisor of 'x'.
|
UniqueFactorizationMonoid.irreducible_of_normalized_factor
theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a : α},
∀ x ∈ UniqueFactorizationMonoid.normalizedFactors a, Irreducible x
This theorem states that for any type `α` that has the structure of a `CancelCommMonoidWithZero`, a `NormalizationMonoid`, and a `UniqueFactorizationMonoid`, and for any element `a` of that type `α`, every element `x` in the multiset of normalized factors of `a` is irreducible. In mathematical terms, this corresponds to the fact that in any unique factorization domain, the prime factors of an element (after being normalized) are irreducible.
More concisely: In a type `α` equipped with the structures of a `CancelCommMonoidWithZero`, a `NormalizationMonoid`, and a `UniqueFactorizationMonoid`, every normalized factor of any element `a` is irreducible.
|
Associates.eq_pow_count_factors_of_dvd_pow
theorem Associates.eq_pow_count_factors_of_dvd_pow :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
[inst_2 : (p : Associates α) → Decidable (Irreducible p)] [inst_3 : DecidableEq (Associates α)]
{p a : Associates α}, Irreducible p → ∀ {n : ℕ}, a ∣ p ^ n → a = p ^ p.count a.factors
The theorem `Associates.eq_pow_count_factors_of_dvd_pow` states that in a commutative cancellative monoid with zero that also has unique factorization, for any irreducible element `p` and any other element `a` of the `Associates` of that monoid, if `a` divides some power of `p`, then `a` is also a power of `p`. Specifically, the exponent of this power is equal to the count of `p` in the factorization of `a`. Here, `Associates` refers to the quotient of a monoid by the `Associated` relation, where two elements `x` and `y` are associated if there exists a unit `u` such that `x * u = y`. Decidability of irreducibility of `p` and equality in the `Associates` is also assumed.
More concisely: In a commutative cancellative monoid with zero and unique factorization, if an irreducible element `p` is associated with an element `a` and `a` divides some power of `p`, then `a` is a power of `p` with the same exponent as the count of `p` in the factorization of `a`.
|
WfDvdMonoid.exists_irreducible_factor
theorem WfDvdMonoid.exists_irreducible_factor :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : WfDvdMonoid α] {a : α},
¬IsUnit a → a ≠ 0 → ∃ i, Irreducible i ∧ i ∣ a
This theorem states that for any commutative monoid with zero `α` which is also a well-founded divisible monoid, given an element `a` of `α` which is not a unit and is not zero, there exists an irreducible element `i` in `α` that is a factor of `a`. Here, an irreducible element is one that cannot be factored into two non-unit elements, and a well-founded divisible monoid is a structure where the divisibility relation is well-founded (i.e., there are no infinite descending chains).
More concisely: In a commutative monoid with zero that is both well-founded and divisible, every non-zero, non-unit element can be factored into irreducible elements.
|
ufm_of_gcd_of_wfDvdMonoid
theorem ufm_of_gcd_of_wfDvdMonoid :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : WfDvdMonoid α] [inst_2 : DecompositionMonoid α],
UniqueFactorizationMonoid α
This theorem, `ufm_of_gcd_of_wfDvdMonoid`, states that for any type `α` which has the properties of a `CancelCommMonoidWithZero`, a `WfDvdMonoid`, and a `DecompositionMonoid`, it also has the property of being a `UniqueFactorizationMonoid`. This means that any element of `α` can be factored into a unique product of irreducible elements. The theorem cannot be an instance because it would cause a recursive loop: `UniqueFactorizationMonoid` implies `WfDvdMonoid`, which then implies `UniqueFactorizationMonoid`, and so on.
More concisely: If `α` is a type with the properties of a CancelCommMonoidWithZero, a WfDvdMonoid, and a DecompositionMonoid, then `α` is a UniqueFactorizationMonoid.
|
factorization_mul
theorem factorization_mul :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
[inst_2 : NormalizationMonoid α] [inst_3 : DecidableEq α] {a b : α},
a ≠ 0 → b ≠ 0 → factorization (a * b) = factorization a + factorization b
This theorem states that for non-zero elements `a` and `b` from a type `α`, which is a cancellation commutative monoid with zero, a unique factorization monoid, a normalization monoid, and has decidable equality, the factorization of the product `a * b` is equivalent to the sum of the factorizations of `a` and `b`. In other words, in such a monoid, the power of a prime factor `p` in the product of `a` and `b` is the sum of the powers of `p` in `a` and `b`. This is an expression of the fundamental theorem of arithmetic, which says that the factorization of a product of two numbers is the sum of the factorizations of the numbers.
More concisely: In a cancellation commutative monoid with zero, unique factorization, normalization, and decidable equality, the factorization of the product of non-zero elements is equal to the sum of their factorizations.
|
Associates.factors_one
theorem Associates.factors_one :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : Nontrivial α],
Associates.factors 1 = 0
This theorem, `Associates.factors_one`, states that for any type `α` that forms a `CancelCommMonoidWithZero` and a `UniqueFactorizationMonoid` and is nontrivial, the multiset of irreducible factors of the associate of `1` (which is itself) is `0`. In other words, `1` has no irreducible factors, which aligns with the mathematical concept that `1` is not considered a prime or irreducible number.
More concisely: In a nontrivial `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid` type `α`, the set of irreducible factors of `1` is empty.
|
Associates.eq_pow_find_of_dvd_irreducible_pow
theorem Associates.eq_pow_find_of_dvd_irreducible_pow :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : Associates α},
Irreducible p → ∀ [inst_2 : (n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n), a = p ^ Nat.find ⋯
This theorem states that in a unique factorization monoid with zero cancellation property, for any associates of the monoid `a` and `p` where `p` is irreducible, if `a` divides a power of `p`, then `a` must be a power of `p` itself. The exponent of this power of `p` is determined by the natural number `n` that is found by a decidability process for whether `a` divides `p` to the power of `n`. This is a reflection of the principle that the only divisors of prime powers are prime powers themselves.
More concisely: In a unique factorization monoid with zero cancellation property, if an associates of an irreducible element `p` divides `p` raised to some power, then it is itself a power of `p`.
|
UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a p : α},
a ≠ 0 → Irreducible p → p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors a, Associated p q
This theorem states that for any non-zero element `a` of a unique factorization monoid, given an irreducible element `p` that divides `a`, there exists an element `q` in the multiset of normalized prime factors of `a` such that `p` and `q` are associated. In other words, if `p` is an irreducible factor of `a`, there must be an equivalent factor in the prime factorization of `a`. The equivalence is determined by the `Associated` relation, meaning `p` and `q` are equivalent if `p` can be obtained by multiplying `q` by a unit of the monoid.
More concisely: For any non-zero element `a` in a unique factorization monoid and any irreducible factor `p` of `a`, there exists a normalized prime factor `q` of `a` such that `p` and `q` are associated.
|
support_factorization
theorem support_factorization :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
[inst_2 : NormalizationMonoid α] [inst_3 : DecidableEq α] {n : α},
(factorization n).support = (UniqueFactorizationMonoid.normalizedFactors n).toFinset
The theorem `support_factorization` states that for any type `α` that is a `CancelCommMonoidWithZero`, `UniqueFactorizationMonoid`, and `NormalizationMonoid`, and has decidable equality, and for any element `n` of `α`, the support of the factorization of `n` is exactly equal to the finset obtained from the normalized factors of `n` in `UniqueFactorizationMonoid`. In simpler terms, all the factors that appear in the factorization of `n` are exactly the normalized irreducible factors of `n`.
More concisely: For any `CancelCommMonoidWithZero`, `UniqueFactorizationMonoid`, and `NormalizationMonoid` type `α` with decidable equality, the support of `n`'s factorization equals the finset of normalized irreducible factors of `n` in `α`.
|
factorization_pow
theorem factorization_pow :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
[inst_2 : NormalizationMonoid α] [inst_3 : DecidableEq α] {x : α} {n : ℕ},
factorization (x ^ n) = n • factorization x
This theorem states that for any element `p`, the power of `p` in `x^n` is `n` times the power in `x`. In this context, `α` is a type that satisfies the constraints of being a cancel commutative monoid with zero, a unique factorization monoid, a normalization monoid, and having decidable equality. `x` is an element of `α`, and `n` is a natural number. The `factorization` function returns a finite-support function that represents the multiset of irreducible factors of a given element. In the case of `x^n`, the factorization is equal to `n` times the factorization of `x`, which means that the exponent of each irreducible factor in the factorization of `x^n` is `n` times the exponent in the factorization of `x`.
More concisely: For any element `x` in a cancellative, commutative monoid `α` with zero, unique factorization, normalization, and decidable equality, the power `x^n` has the same irreducible factorization as `n` times the power `x^1`.
|
Associates.factors_mono
theorem Associates.factors_mono :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : Associates α},
a ≤ b → a.factors ≤ b.factors
The theorem `Associates.factors_mono` states that for any type `α` that has a `CancelCommMonoidWithZero` structure and a `UniqueFactorizationMonoid` structure, and for any two elements `a` and `b` of the `Associates` of `α`, if `a` is less than or equal to `b`, then the multiset of irreducible factors of `a` (represented as a `FactorSet`) is less than or equal to the multiset of irreducible factors of `b`. Here, the `≤` relation for `FactorSets` is defined in terms of the associated partial order on multisets.
More concisely: For any type `α` with `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid` structures, if `a` and `b` are associates in `α` with `a ≤ b`, then the multiset of irreducible factors of `a` is less than or equal to the multiset of irreducible factors of `b` according to the partial order on multisets.
|
UniqueFactorizationMonoid.prime_of_normalized_factor
theorem UniqueFactorizationMonoid.prime_of_normalized_factor :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a : α}, ∀ x ∈ UniqueFactorizationMonoid.normalizedFactors a, Prime x
This theorem states that in any Unique Factorization Monoid which is also a Cancel Commutative Monoid With Zero and a Normalization Monoid, for any element 'a' of that monoid, any element 'x' that is a member of the multiset of normalized factors of 'a', is a prime element. A prime element is defined as an element that is not zero, is not a unit, and has the property that if it divides the product of two other elements, it must divide at least one of those elements.
More concisely: In a Unique Factorization, Cancel Commutative Monoid with Zero and Normalization property, every normalized factor of any element is a prime.
|
UniqueFactorizationMonoid.normalizedFactors_mul
theorem UniqueFactorizationMonoid.normalizedFactors_mul :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {x y : α},
x ≠ 0 →
y ≠ 0 →
UniqueFactorizationMonoid.normalizedFactors (x * y) =
UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y
This theorem states that for any type `α` that is a `CancelCommMonoidWithZero`, a `NormalizationMonoid`, and a `UniqueFactorizationMonoid`, and for any non-zero elements `x` and `y` of type `α`, the multiset of normalized prime factors of the product `x * y` is equal to the sum of the multisets of normalized prime factors of `x` and `y`. This reflects the fundamental property of prime factorization, stating that the prime factorization of a product is the concatenation of the prime factorizations of the factors, in the context of a `UniqueFactorizationMonoid`.
More concisely: In a `CancelCommMonoidWithZero`, `NormalizationMonoid`, and `UniqueFactorizationMonoid` `α`, the multiset of normalized prime factors of the product of any two non-zero elements `x` and `y` is equal to the sum of the multisets of normalized prime factors of `x` and `y`.
|
UniqueFactorizationMonoid.exists_reduced_factors
theorem UniqueFactorizationMonoid.exists_reduced_factors :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] (a : R),
a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
This theorem states that if we have a non-zero element `a` and another element `b` in a unique factorization domain, then there exist elements `a'`, `b'` and `c'` such that `a'` and `b'` have no common factors (they are relatively prime), and `a` and `b` are products of `c'` and `a'`, `b'` respectively. A unique factorization domain is a type of mathematical structure where every non-zero non-unit element can be uniquely written as a product of irreducible elements, up to order and units. The "relatively prime" condition implies that the only common divisor of `a'` and `b'` is a unit.
More concisely: In a unique factorization domain, every pair of non-zero, non-unit elements can be written as a product of relatively prime elements.
|
UniqueFactorizationMonoid.multiplicative_of_coprime
theorem UniqueFactorizationMonoid.multiplicative_of_coprime :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {β : Type u_3}
[inst_2 : CancelCommMonoidWithZero β] (f : α → β) (a b : α),
f 0 = 0 →
(∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) →
(∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) →
(∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) → f (a * b) = f a * f b
This theorem states that if a function `f` from a unique factorization monoid `α` to a cancel commutative monoid with zero `β` satisfies the following conditions: it maps zero to zero, it is multiplicative on units, it maps `p ^ i` to `(f p) ^ i` for each prime `p` and natural number `i`, and it is multiplicative on coprime elements, then `f` is multiplicative everywhere. In other words, if `f` behaves in these specific ways with respect to the structure of the monoids and the concepts of prime and coprime elements, then for any elements `a` and `b` in `α`, `f(a * b)` is equal to `f(a) * f(b)`.
More concisely: If `f` is a function from a unique factorization monoid to a commutative monoid with zero, such that `f(0) = 0`, `f` maps units to units, and `f(p^i) = (f p)^i` for primes `p` and natural numbers `i`, then `f` is multiplicative, i.e., `f(ab) = f(a) * f(b)` for all `a, b` in the monoid.
|
UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {x y : α},
x ≠ 0 →
y ≠ 0 →
(x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y)
This theorem states that for any types `α` that form a `CancelCommMonoidWithZero`, a `NormalizationMonoid`, and a `UniqueFactorizationMonoid`, and for any two nonzero elements `x` and `y` of type `α`, the element `x` divides `y` if and only if the multiset of normalized prime factors of `x` is less than or equal to the multiset of normalized prime factors of `y`. Here, 'less than or equal to' is in the multiset sense, meaning every prime factor of `x` (with its multiplicity) is also a prime factor of `y` (with equal or greater multiplicity).
More concisely: For any type `α` that is a `CancelCommMonoidWithZero`, `NormalizationMonoid`, and `UniqueFactorizationMonoid`, two nonzero elements `x` and `y` of type `α` are related by `x | y` if and only if the multisets of normalized prime factors of `x` are less than or equal to those of `y`.
|
Associates.prod_mono
theorem Associates.prod_mono :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a b : Associates.FactorSet α}, a ≤ b → a.prod ≤ b.prod := by
sorry
The theorem `Associates.prod_mono` states that for any type `α` that has the structure of a `CancelCommMonoidWithZero`, and for any two `FactorSet`s `a` and `b` of `Associates` of `α`, if `a` is less than or equal to `b` then the product of `FactorSet` `a` is less than or equal to the product of `FactorSet` `b`. Here, the product of a `FactorSet` is defined as the product of the corresponding multiset, or `0` if there is none. The order relation on `FactorSet`s is induced by the order relation on `Associates`.
More concisely: For any type `α` with the structure of a `CancelCommMonoidWithZero` and for any `Associates` `FactorSet`s `a` and `b`, if `a` is less than or equal to `b`, then the product of `a` is less than or equal to the product of `b`.
|
UniqueFactorizationMonoid.factors_prod
theorem UniqueFactorizationMonoid.factors_prod :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
a ≠ 0 → Associated (UniqueFactorizationMonoid.factors a).prod a
The theorem `UniqueFactorizationMonoid.factors_prod` in Lean 4 states that for all non-zero elements `a` of any Type `α` that forms a CancelCommMonoidWithZero and a UniqueFactorizationMonoid, `a` is associated with the product of its prime factors. That is, `a` can be written as a product of its prime factors times some unit. In the context of number theory, this roughly translates to the unique factorization theorem, also known as the fundamental theorem of arithmetic, which states that every integer greater than 1 is either a prime number itself or can be factorized as a product of prime numbers.
More concisely: Every non-zero element in a Type α that is both a cancel commutative monoid with identity and a unique factorization monoid can be expressed as the product of its prime factors up to units.
|
UniqueFactorizationMonoid.normalizedFactors_zero
theorem UniqueFactorizationMonoid.normalizedFactors_zero :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α], UniqueFactorizationMonoid.normalizedFactors 0 = 0
This theorem states that for any type `α` that forms a `CancelCommMonoidWithZero`, a `NormalizationMonoid`, and a `UniqueFactorizationMonoid`, the multiset of normalized prime factors of zero, as determined by the `UniqueFactorizationMonoid.normalizedFactors` function, is zero. In other words, the zero element has no prime factors in the context of unique factorization monoids.
More concisely: For any type `α` that is a CancelCommMonoidWithZero, a NormalizationMonoid, and a UniqueFactorizationMonoid in Lean 4, the normalized prime factors of zero, as given by `UniqueFactorizationMonoid.normalizedFactors`, are the empty multiset.
|
Associates.eq_of_prod_eq_prod
theorem Associates.eq_of_prod_eq_prod :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : Nontrivial α]
{a b : Associates.FactorSet α}, a.prod = b.prod → a = b
This theorem, `Associates.eq_of_prod_eq_prod`, states that for any type `α` that has the structure of a `CancelCommMonoidWithZero` (a commutative monoid with a zero element which also has the cancellation property), a `UniqueFactorizationMonoid` (a monoid that has unique factorization into irreducible elements), and is `Nontrivial` (it has at least two distinct elements), if we have two `FactorSet` objects `a` and `b` from `Associates` of `α`, and the product of the factors of `a` is equal to the product of factors of `b` (computed using the `Associates.FactorSet.prod` function), then `a` and `b` must be equal. In other words, two factor sets are equal if and only if their product of factors are equal under the given algebraic structures.
More concisely: For any commutative monoid with a zero element, unique factorization, and at least two distinct elements `α` with associated factor sets `a` and `b` satisfying `Associates.prod a = Associates.prod b`, we have `a = b`.
|
WfDvdMonoid.exists_factors
theorem WfDvdMonoid.exists_factors :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : WfDvdMonoid α] (a : α),
a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a
The theorem `WfDvdMonoid.exists_factors` states that in any well-founded commutative monoid with zero, given a nonzero element `a`, there exist a multiset `f` of irreducible elements such that every element in `f` is irreducible and the product of all elements in `f` is associated with `a`. In other words, every nonzero element `a` in such a monoid can be expressed as a product of irreducible elements, up to an association. This is akin to the idea of prime factorization in the integers, where every integer can be expressed as a product of prime numbers (which are irreducible).
More concisely: In a commutative well-founded monoid with zero, every nonzero element can be expressed as the product of irreducible elements, up to association.
|
UniqueFactorizationMonoid.normalizedFactors_prod
theorem UniqueFactorizationMonoid.normalizedFactors_prod :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a : α},
a ≠ 0 → Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
This theorem states that for any non-zero element 'a' in a ring that is additionally a unique factorization monoid and normalization monoid, the product of its normalized factors is associated with 'a' itself.
Here, 'associated' means that you can get from one element to the other by multiplying by a unit from the ring. A 'unit' in this context is an element that has a multiplicative inverse.
This is essentially a version of the fundamental theorem of arithmetic, stating that every non-zero integer can be uniquely expressed (up to the order of the factors) as a product of prime numbers, for the general setting of a unique factorization monoid.
More concisely: In a unique factorization monoid and normalization monoid ring, the normalized product of any non-zero element equals the element itself, up to associating with units.
|
UniqueFactorizationMonoid.factors_unique
theorem UniqueFactorizationMonoid.factors_unique :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {f g : Multiset α},
(∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g
The theorem `UniqueFactorizationMonoid.factors_unique` states that for a given Type `α` which has a `CancelCommMonoidWithZero` and `UniqueFactorizationMonoid` structure, if we have two multisets `f` and `g`, where all elements in both multisets are irreducible, then if the product of all elements in `f` is associated with the product of all elements in `g` (meaning that one product can be gotten by multiplying the other by a unit), then each element in `f` is associated with an element in `g`, and vice versa. This is the uniqueness part of the unique factorization property in algebra, stating that every element in a unique factorization monoid can be uniquely factored into irreducible elements (up to association).
More concisely: In a unique factorization monoid with cancellation, if two multisets of irreducible elements have the same product up to units, then each irreducible in one multiset is associated with exactly one irreducible in the other multiset.
|
Associates.factors_mk
theorem Associates.factors_mk :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
a ≠ 0 → (Associates.mk a).factors = ↑(Associates.factors' a)
The theorem `Associates.factors_mk` states that for any non-zero element `a` of a type `α`, where `α` is assumed to be a cancel commutative monoid with zero and has the property of unique factorization, the multiset of irreducible factors of the associate of `a` is equal to the multiset of irreducible factors of `a` itself. In mathematical terms, this means that the process of associating does not change the irreducible factors of `a` if `a` is nonzero.
More concisely: For any non-zero element `a` in a cancel commutative monoid `α` with unique factorization, the multiset of irreducible factors of `a` is equal to the multiset of irreducible factors of its associate.
|
UniqueFactorizationMonoid.induction_on_coprime
theorem UniqueFactorizationMonoid.induction_on_coprime :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {P : α → Prop} (a : α),
P 0 →
(∀ {x : α}, IsUnit x → P x) →
(∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) → (∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) → P a
The theorem `UniqueFactorizationMonoid.induction_on_coprime` states that for any type `α` that is a cancel commutative monoid with zero and a unique factorization monoid, and for any property `P` from `α` to `Prop`, if `P` holds for `0`, for all units, and for all powers of primes, and if `P x` and `P y` implies `P (x * y)` for all coprime `x` and `y`, then `P` holds for all elements `a` of `α`. In simple terms, this theorem provides a way to prove a property holds for all elements of such a monoid by proving it for simpler cases and showing it preserves under multiplication of coprime elements.
More concisely: If `α` is a cancel commutative monoid with zero and a unique factorization monoid, and `P(0)` holds and `P` is preserved under multiplication of coprime elements, then `P` holds for all `α`.
|
UniqueFactorizationMonoid.factors_eq_normalizedFactors
theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors :
∀ {M : Type u_2} [inst : CancelCommMonoidWithZero M] [inst_1 : UniqueFactorizationMonoid M] [inst_2 : Unique Mˣ]
(x : M), UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.normalizedFactors x
This theorem states that, for any type `M` that is a cancel commutative monoid with zero, a unique factorization monoid, and has a trivial group of units, the arbitrary chosen factors of an element `x : M` are exactly the same as the unique normalized set of factors. In other words, the multiset of prime factors, as determined by the `UniqueFactorizationMonoid.factors` function, is identical to the normalized version of these factors, as determined by the `UniqueFactorizationMonoid.normalizedFactors` function.
More concisely: For any cancel commutative monoid with zero, unique factorization property, and trivial unit group, the arbitrary factors of an element equal the normalized unique factors.
|
UniqueFactorizationMonoid.exists_prime_factors
theorem UniqueFactorizationMonoid.exists_prime_factors :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
This theorem states that for any non-zero element `a` in a `CancelCommMonoidWithZero` α that also has a `UniqueFactorizationMonoid` structure, there exists a multiset `f` such that every element `b` in `f` is prime, and the product of all elements in `f` is associated with `a`. In other words, any non-zero element in a unique factorization domain can be factored into a product of prime elements.
More concisely: In a CancelCommMonoidWithZero α equipped with a UniqueFactorizationMonoid structure, any non-zero element can be expressed as the product of a multiset of prime elements.
|
WfDvdMonoid.induction_on_irreducible
theorem WfDvdMonoid.induction_on_irreducible :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : WfDvdMonoid α] {P : α → Prop} (a : α),
P 0 → (∀ (u : α), IsUnit u → P u) → (∀ (a i : α), a ≠ 0 → Irreducible i → P a → P (i * a)) → P a
This theorem, `WfDvdMonoid.induction_on_irreducible`, is a principle of induction for a well-founded (meaning there are no infinite descending chains) divisibility monoid with zero. Given a type `α` which is equipped with a commutative monoid structure with zero element and is a well-founded divisibility monoid, this theorem states that for any property `P` and any element `a` of `α`, if `P` holds for 0, and if `P` holds for any unit `u` of `α`, and if for any non-zero `a` and any irreducible `i` of `α`, `P` holding for `a` implies that `P` holds for the product of `i` and `a`, then `P` holds for `a`. In other words, it allows one to prove a property about all elements of a well-founded divisibility monoid with zero by considering the cases where the element is 0, a unit, or a product of an irreducible element and another element for which the property holds.
More concisely: Given a well-founded commutative monoid with zero and unit elements, if a property holds for 0 and units, and if it is preserved under multiplication by irreducible elements, then the property holds for all elements.
|
UniqueFactorizationMonoid.multiplicative_prime_power
theorem UniqueFactorizationMonoid.multiplicative_prime_power :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {β : Type u_3}
[inst_2 : CancelCommMonoidWithZero β] {f : α → β} (s : Finset α) (i j : α → ℕ),
(∀ p ∈ s, Prime p) →
(∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) →
(∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) →
(∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) →
(∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) →
f (s.prod fun p => p ^ (i p + j p)) = f (s.prod fun p => p ^ i p) * f (s.prod fun p => p ^ j p)
The theorem `UniqueFactorizationMonoid.multiplicative_prime_power` states that if a function `f` satisfies two properties: (1) for any prime number `p`, it maps `p` to the power of `i` to `(f p)` to the power of `i`, and (2) it behaves multiplicatively on coprime elements (i.e., `f` of the product of two coprime numbers `x` and `y` equals the product of `f(x)` and `f(y)`), then `f` is multiplicative on all products of primes. In other words, if we have a set `s` of prime numbers where each prime `p` is associated with two natural numbers `i` and `j`, then `f` applied to the product of the primes in `s` each raised to the sum of its associated `i` and `j`, equals the product of `f` applied to the product of primes each raised to `i` and `f` applied to the product of primes each raised to `j`. This is under the conditions that all elements of `s` are primes, each prime `p` divides another prime `q` in `s` only if `p` is equal to `q`, and `f` behaves multiplicatively when one of its arguments is a unit.
More concisely: If a multiplicative function `f` maps every prime `p` to the power `i` such that `p` raises to `i` is coprime to the domain, and `f` is multiplicative on coprime elements, then `f` is multiplicative on any product of primes.
|
Associates.mem_factorSet_some
theorem Associates.mem_factorSet_some :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : Associates α} {hp : Irreducible p}
{l : Multiset { a // Irreducible a }}, p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l
The theorem `Associates.mem_factorSet_some` asserts that for any type `α` with a structure of a cancel commutative monoid with zero, any element `p` of the `Associates` of `α` (i.e., the quotient of the monoid `α` by the `Associated` relation), and any multiset `l` of irreducible elements, the element `p` is a member of the underlying set of `l` if and only if it is a member of `l` itself when we consider `p` as an element with the property of irreducibility. In essence, this theorem is about the membership of irreducible elements in multisets, considering both the set and the specific irreducible property of elements.
More concisely: For any cancel commutative monoid with zero `α`, an irreducible element `p` in `α` is a member of a multiset `l` of irreducible elements if and only if `p` is itself a member of `l` when regarded as an element of the underlying set.
|
Associates.prod_coe
theorem Associates.prod_coe :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {s : Multiset { a // Irreducible a }},
Associates.FactorSet.prod ↑s = (Multiset.map Subtype.val s).prod
The theorem `Associates.prod_coe` states that for any type `α` that has a `CancelCommMonoidWithZero` structure and for any multiset `s` of elements `a` which satisfy the property of being irreducible, the product of `s` as an `Associates.FactorSet` is equal to the product of the multiset obtained by mapping the `Subtype.val` function over `s`. In mathematical terms, this theorem shows the consistency between the product of a `FactorSet` and the product of the corresponding multiset of irreducible elements in a commutative monoid with zero.
More concisely: For any commutative monoid with zero `α` and irreducible multiset `s` of elements `a` in `α`, the product of `s` as an `Associates.FactorSet` equals the product of the multiset of `Subtype.val a` for all `a` in `s`.
|
UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors
theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors :
∀ {R : Type u_2} [inst : CancelCommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] {a b c : R},
a ≠ 0 → (∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) → a ∣ b * c → a ∣ c
This theorem is known as Euclid's Lemma. It states that for any type `R` that is a cancel commutative monoid with zero and has unique factorization, given non-zero elements `a`, `b`, and `c` of `R`, if `a` divides the product `b * c` and `a` and `b` have no common prime factors (i.e., for any element `d` of `R` which divides `a` and `b`, `d` is not prime), then `a` also divides `c`. In other words, if a number divides a product, and it has no common prime factors with one of the multiplicands, it must divide the other multiplicand.
More concisely: If `a` divides the product `b * c` in a cancel commutative monoid with unique factorization, and `a` and `b` have no common prime factors, then `a` divides `c`.
|
UniqueFactorizationMonoid.normalizedFactors_irreducible
theorem UniqueFactorizationMonoid.normalizedFactors_irreducible :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α]
[inst_2 : UniqueFactorizationMonoid α] {a : α},
Irreducible a → UniqueFactorizationMonoid.normalizedFactors a = {normalize a}
The theorem `UniqueFactorizationMonoid.normalizedFactors_irreducible` states that for any irreducible element `a` in a unique factorization monoid `α` (a commutative monoid with zero where the only unit multiples of a given element are itself and its associates), the multiset of the normalized (obtained by multiplying by `normUnit`) prime factors of `a` is a singleton set containing only the normalized form of `a`. This essentially means that the irreducible element `a` does not have any other prime factors except for its normalized form.
More concisely: In a unique factorization monoid, the normalized prime factors of an irreducible element form a singleton set.
|
UniqueFactorizationMonoid.irreducible_of_factor
theorem UniqueFactorizationMonoid.irreducible_of_factor :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
∀ x ∈ UniqueFactorizationMonoid.factors a, Irreducible x
This theorem states that for any type `α` that has both a `CancelCommMonoidWithZero` and a `UniqueFactorizationMonoid` structure, any element `x` that appears in the multiset of prime factors of another element `a` of the type `α` is irreducible. The term "irreducible" in this context refers to elements that cannot be expressed as a product of two non-unit elements. This is a key property of prime factors in the context of unique factorization domains, essentially saying that the prime factors of a number are themselves prime.
More concisely: For any type `α` equipped with both a `CancelCommMonoidWithZero` and a `UniqueFactorizationMonoid` structure, every prime factor is irreducible.
|