PNat.factorMultiset_gcd
theorem PNat.factorMultiset_gcd : ∀ (m n : ℕ+), (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset := by
sorry
This theorem states that for any two positive integers `m` and `n`, the factor multiset of the greatest common divisor (gcd) of `m` and `n` is equivalent to the intersection of the factor multisets of `m` and `n`. In other words, the factorization of the gcd of two numbers is composed of the common factors of the two numbers. This theorem links the concepts of gcd and lcm to the operations on multisets, treating the factorizations as multisets and using the intersection and union operations.
More concisely: The factor multisets of the greatest common divisor of two positive integers are equal to the intersection of their factor multisets.
|
PNat.factorMultiset_one
theorem PNat.factorMultiset_one : PNat.factorMultiset 1 = 0
The theorem `PNat.factorMultiset_one` states that factoring operation acts as a homomorphism from the multiplicative monoid of positive natural numbers (ℕ+) to the additive monoid of multisets. Specifically, it states that the multiset of prime factors of the number 1 is an empty multiset, represented by 0 in this context. In other words, the number 1 has no prime factors, which is reflected in the fact that the factor multiset of 1 is the additive identity in the monoid of multisets.
More concisely: The theorem `PNat.factorMultiset_one` asserts that the multiset of prime factors of 1 is the additive identity in the monoid of multisets of natural numbers. In other words, the factor multiset of 1 is the empty multiset.
|
PrimeMultiset.prod_zero
theorem PrimeMultiset.prod_zero : PrimeMultiset.prod 0 = 1
The theorem `PrimeMultiset.prod_zero` states that the product of an empty `PrimeMultiset` is 1. Here, `PrimeMultiset.prod` is a function that gives the product of all elements in a `PrimeMultiset` (a certain type of multi-set consisting of prime numbers). The theorem essentially says that this function behaves as a homomorphism from the additive monoid of multisets to the multiplicative monoid of positive natural numbers (ℕ+), specifically stating the property that the product of the zero element in the additive monoid (the empty multiset) is the identity element in the multiplicative monoid (1).
More concisely: The empty PrimeMultiset multiplicatively identities the product of prime numbers.
|
PNat.prod_factorMultiset
theorem PNat.prod_factorMultiset : ∀ (n : ℕ+), n.factorMultiset.prod = n
This theorem states that for any given positive natural number `n`, the product of its prime factors, when considered as a multiset, equals the original number `n`. In mathematical terms, it's saying that if you decompose a positive integer into its prime factors and then multiply those prime factors together, you will get back the original number. This is a fundamental property of prime factorization.
More concisely: The product of the prime factors of a positive integer, each raised to the power of their multiplicity in its prime factorization, equals the original integer.
|
PNat.factorMultiset_le_iff
theorem PNat.factorMultiset_le_iff : ∀ {m n : ℕ+}, m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n
This theorem is expressing the relationship between the inequality of multisets of prime factors of positive integers and the divisibility of these positive integers. More specifically, for any two positive integers `m` and `n`, the multiset of prime factors of `m` being less than or equal to the multiset of prime factors of `n` is equivalent to `m` dividing `n`. This theorem encapsulates one aspect of the fundamental theorem of arithmetic, namely that each integer has a unique prime factorization, and relates it to the concept of divisibility.
More concisely: The multiset of prime factors of a positive integer `m` being less than or equal to the multiset of prime factors of a positive integer `n` if and only if `m` divides `n`.
|
PrimeMultiset.prod_add
theorem PrimeMultiset.prod_add : ∀ (u v : PrimeMultiset), (u + v).prod = u.prod * v.prod
The theorem `PrimeMultiset.prod_add` states that for any two prime multisets `u` and `v`, the product of the multiset obtained by adding `u` and `v` is equal to the product of the multiset `u` multiplied by the product of the multiset `v`. In other words, if you have two collections of prime numbers (represented as multisets), the product of all the primes in the combined collection is the same as the product of all the primes in the first collection multiplied by the product of all the primes in the second collection. This is a reflection of the fundamental property of multiplication being distributive over addition.
More concisely: For any prime multisets u and v, (u ⊎ v) := {p : ℕ | p ∈ u ∨ p ∈ v} → ∏ (p : ℕ) in p = ∏ p in u * ∏ p in v, where ℕ is the set of natural numbers.
|
PNat.count_factorMultiset
theorem PNat.count_factorMultiset :
∀ (m : ℕ+) (p : Nat.Primes) (k : ℕ), ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset
This theorem states that for any positive natural number `m`, any prime number `p`, and any natural number `k`, the power of `p` to the `k`th power divides `m` if and only if `k` is less than or equal to the count of `p` in the factor multiset of `m`. In other words, it's a characterization of the p-adic valuation, which measures how many times a number `m` is divisible by a prime `p`. It's saying that the number of times `m` is divisible by `p` is the same as the number of times `p` appears in the prime factorization of `m`.
More concisely: For any positive integer m, prime number p, and natural number k, the power of p to the kth power divides m if and only if the count of p in the prime factorization of m is less than or equal to k.
|
PrimeMultiset.prod_dvd_iff
theorem PrimeMultiset.prod_dvd_iff : ∀ {u v : PrimeMultiset}, u.prod ∣ v.prod ↔ u ≤ v
The theorem `PrimeMultiset.prod_dvd_iff` states that for any two multisets of prime numbers `u` and `v`, the product of the elements of `u` divides the product of the elements of `v` if and only if `u` is a sub-multiset of `v`. In other words, every prime number in `u` also appears in `v`, possibly with fewer occurrences.
More concisely: For multisets of prime numbers `u` and `v`, `prod u ∣ prod v` if and only if `u` is a sub-multiset of `v`.
|
PNat.factorMultiset_ofPrime
theorem PNat.factorMultiset_ofPrime : ∀ (p : Nat.Primes), (↑p).factorMultiset = PrimeMultiset.ofPrime p
The theorem `PNat.factorMultiset_ofPrime` states that for all prime numbers `p`, the multiset of prime factors of `p` is equivalent to the multiset constructed from the prime number `p` itself. In other words, when a prime number is factored, the resulting multiset only contains that prime number itself, which validates the concept that prime numbers have only one prime factor, which is the number itself.
More concisely: For every prime number `p`, the multiset of its prime factors is equal to the multiset consisting of `p` itself.
|
PrimeMultiset.factorMultiset_prod
theorem PrimeMultiset.factorMultiset_prod : ∀ (v : PrimeMultiset), v.prod.factorMultiset = v
This theorem states that for any multiset of prime numbers, if we compute the product of these prime numbers into a positive natural number and then factorize this product back into its prime factors, we will retrieve the original multiset of prime numbers. In essence, this process demonstrates a round-trip property of prime factorization and product, which is the fundamental principle of the unique factorization theorem in number theory.
More concisely: Given any multiset of prime numbers, the product of these primes and the prime factorization of the result are equal.
|