Chains of divisors #
The results in this file show that in the monoid
Associates M of a
M, an element
a is an n-th prime power iff its set of divisors is a strictly increasing chain
n + 1, meaning that we can find a strictly increasing bijection between
Fin (n + 1)
and the set of factors of
Main results #
DivisorChain.exists_chain_of_prime_pow: existence of a chain for prime powers.
DivisorChain.is_prime_pow_of_has_chain: elements that have a chain are prime powers.
multiplicity_prime_eq_multiplicity_image_by_factor_orderIso: if there is a monotone bijection
dbetween the set of factors of
a : Associates Mand the set of factors of
b : Associates Nthen for any prime
p ∣ a,
multiplicity p a = multiplicity (d p) b.
multiplicity_eq_multiplicity_factor_dvd_iso_of_mem_normalizedFactors: if there is a bijection between the set of factors of
a : Mand
b : Nthen for any prime
p ∣ a,
multiplicity p a = multiplicity (d p) b
- Create a structure for chains of divisors.
- Simplify proof of
mem_normalizedFactors_factor_order_iso_of_mem_normalizedFactorsor vice versa.
The second element of a chain is irreducible.
The order isomorphism between the factors of
mk m and the factors of
mk n induced by a
bijection between the factors of
m and the factors of
n that preserves