Documentation

Mathlib.RingTheory.UniqueFactorizationDomain

Unique factorization #

Main Definitions #

To do #

class WfDvdMonoid (α : Type u_2) [CommMonoidWithZero α] :

Well-foundedness of the strict version of |, which is equivalent to the descending chain condition on divisibility and to the ascending chain condition on principal ideals in an integral domain.

Instances
    @[instance 100]
    Equations
    • =
    theorem WfDvdMonoid.exists_irreducible_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a : α} (ha : ¬IsUnit a) (ha0 : a 0) :
    ∃ (i : α), Irreducible i i a
    theorem WfDvdMonoid.induction_on_irreducible {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {P : αProp} (a : α) (h0 : P 0) (hu : ∀ (u : α), IsUnit uP u) (hi : ∀ (a i : α), a 0Irreducible iP aP (i * a)) :
    P a
    theorem WfDvdMonoid.exists_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) :
    a 0∃ (f : Multiset α), (bf, Irreducible b) Associated f.prod a
    theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a 0) :
    ¬IsUnit a ∃ (f : Multiset α), (bf, Irreducible b) f.prod = a f
    theorem WfDvdMonoid.isRelPrime_of_no_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {x : α} {y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), Irreducible zz x¬z y) :
    theorem WfDvdMonoid.max_power_factor' {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ : α} {x : α} (h : a₀ 0) (hx : ¬IsUnit x) :
    ∃ (n : ) (a : α), ¬x a a₀ = x ^ n * a
    theorem WfDvdMonoid.max_power_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ : α} {x : α} (h : a₀ 0) (hx : Irreducible x) :
    ∃ (n : ) (a : α), ¬x a a₀ = x ^ n * a
    theorem multiplicity.finite_of_not_isUnit {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] {a : α} {b : α} (ha : ¬IsUnit a) (hb : b 0) :

    unique factorization monoids.

    These are defined as CancelCommMonoidWithZeros with well-founded strict divisibility relations, but this is equivalent to more familiar definitions:

    Each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.

    Each element (except zero) is non-uniquely represented as a multiset of prime factors.

    To define a UFD using the definition in terms of multisets of irreducible factors, use the definition of_exists_unique_irreducible_factors

    To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

    Instances

      Can't be an instance because it would cause a loop ufmWfDvdMonoidufm → ....

      @[deprecated ufm_of_decomposition_of_wfDvdMonoid]

      Alias of ufm_of_decomposition_of_wfDvdMonoid.


      Can't be an instance because it would cause a loop ufmWfDvdMonoidufm → ....

      theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :
      a 0∃ (f : Multiset α), (bf, Prime b) Associated f.prod a
      theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : αProp} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), IsUnit xP x) (h₃ : ∀ (a p : α), a 0Prime pP aP (p * a)) :
      P a
      theorem prime_factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] {f : Multiset α} {g : Multiset α} :
      (xf, Prime x)(xg, Prime x)Associated f.prod g.prodMultiset.Rel Associated f g
      theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f : Multiset α} {g : Multiset α} (hf : xf, Irreducible x) (hg : xg, Irreducible x) (h : Associated f.prod g.prod) :
      Multiset.Rel Associated f g
      theorem prime_factors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {f : Multiset α} (ha : Irreducible a) (pfa : (bf, Prime b) Associated f.prod a) :
      ∃ (p : α), Associated a p f = {p}

      If an irreducible has a prime factorization, then it is an associate of one of its prime factors.

      theorem WfDvdMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a 0∃ (f : Multiset α), (bf, Prime b) Associated f.prod a) :
      theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a 0∃ (f : Multiset α), (bf, Prime b) Associated f.prod a) {p : α} :
      theorem UniqueFactorizationMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a 0∃ (f : Multiset α), (bf, Prime b) Associated f.prod a) :
      theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] :
      UniqueFactorizationMonoid α ∀ (a : α), a 0∃ (f : Multiset α), (bf, Prime b) Associated f.prod a
      theorem irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a 0∃ (f : Multiset α), (bf, Irreducible b) Associated f.prod a) (uif : ∀ (f g : Multiset α), (xf, Irreducible x)(xg, Irreducible x)Associated f.prod g.prodMultiset.Rel Associated f g) (p : α) :
      theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a 0∃ (f : Multiset α), (bf, Irreducible b) Associated f.prod a) (uif : ∀ (f g : Multiset α), (xf, Irreducible x)(xg, Irreducible x)Associated f.prod g.prodMultiset.Rel Associated f g) :

      Noncomputably determines the multiset of prime factors.

      Equations
      Instances For

        Noncomputably determines the multiset of prime factors.

        Equations
        Instances For
          @[simp]

          An arbitrary choice of factors of x : M is exactly the (unique) normalized set of factors, if M has a trivial group of units.

          Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} (ha : a 0) :
            IsRelPrime a b ∀ ⦃d : R⦄, d ad b¬Prime d
            theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} {c : R} (ha : a 0) (h : ∀ ⦃d : R⦄, d ad c¬Prime d) :
            a b * ca b

            Euclid's lemma: if a ∣ b * c and a and c have no common prime factors, a ∣ b. Compare IsCoprime.dvd_of_dvd_mul_left.

            theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} {c : R} (ha : a 0) (no_factors : ∀ {d : R}, d ad b¬Prime d) :
            a b * ca c

            Euclid's lemma: if a ∣ b * c and a and b have no common prime factors, a ∣ c. Compare IsCoprime.dvd_of_dvd_mul_right.

            theorem UniqueFactorizationMonoid.exists_reduced_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) :
            a 0∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' c' * a' = a c' * b' = b

            If a ≠ 0, b are elements of a unique factorization domain, then dividing out their common factor c' gives a' and b' with no factors in common.

            theorem UniqueFactorizationMonoid.exists_reduced_factors' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) (b : R) (hb : b 0) :
            ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' c' * a' = a c' * b' = b
            theorem UniqueFactorizationMonoid.pow_eq_pow_iff {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} (ha0 : a 0) (ha1 : ¬IsUnit a) {i : } {j : } :
            a ^ i = a ^ j i = j

            The multiplicity of an irreducible factor of a nonzero element is exactly the number of times the normalized factor occurs in the normalizedFactors.

            See also count_normalizedFactors_eq which expands the definition of multiplicity to produce a specification for count (normalizedFactors _) _..

            theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : Irreducible p) (hnorm : normalize p = p) {n : } (hle : p ^ n x) (hlt : ¬p ^ (n + 1) x) :

            The number of times an irreducible factor p appears in normalizedFactors x is defined by the number of times it divides x.

            See also multiplicity_eq_count_normalizedFactors if n is given by multiplicity p x.

            theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : p = 0 Irreducible p) (hnorm : normalize p = p) {n : } (hle : p ^ n x) (hlt : ¬p ^ (n + 1) x) :

            The number of times an irreducible factor p appears in normalizedFactors x is defined by the number of times it divides x. This is a slightly more general version of UniqueFactorizationMonoid.count_normalizedFactors_eq that allows p = 0.

            See also multiplicity_eq_count_normalizedFactors if n is given by multiplicity p x.

            @[deprecated WfDvdMonoid.max_power_factor]
            theorem UniqueFactorizationMonoid.max_power_factor {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a₀ : R} {x : R} (h : a₀ 0) (hx : Irreducible x) :
            ∃ (n : ) (a : R), ¬x a a₀ = x ^ n * a

            Deprecated. Use WfDvdMonoid.max_power_factor instead.

            theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {s : Finset α} (i : α) (p : α) (hps : ps) (is_prime : qinsert p s, Prime q) (is_coprime : qinsert p s, q'insert p s, q q'q = q') :
            IsRelPrime (p ^ i p) (p's, p' ^ i p')
            theorem UniqueFactorizationMonoid.induction_on_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : αProp} (s : Finset α) (i : α) (is_prime : ps, Prime p) (is_coprime : ps, qs, p qp = q) (h1 : ∀ {x : α}, IsUnit xP x) (hpr : ∀ {p : α} (i : ), Prime pP (p ^ i)) (hcp : ∀ {x y : α}, IsRelPrime x yP xP yP (x * y)) :
            P (ps, p ^ i p)

            If P holds for units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on a product of powers of distinct primes.

            theorem UniqueFactorizationMonoid.induction_on_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : αProp} (a : α) (h0 : P 0) (h1 : ∀ {x : α}, IsUnit xP x) (hpr : ∀ {p : α} (i : ), Prime pP (p ^ i)) (hcp : ∀ {x y : α}, IsRelPrime x yP xP yP (x * y)) :
            P a

            If P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.

            theorem UniqueFactorizationMonoid.multiplicative_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] {f : αβ} (s : Finset α) (i : α) (j : α) (is_prime : ps, Prime p) (is_coprime : ps, qs, p qp = q) (h1 : ∀ {x y : α}, IsUnit yf (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ), Prime pf (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, IsRelPrime x yf (x * y) = f x * f y) :
            f (ps, p ^ (i p + j p)) = f (ps, p ^ i p) * f (ps, p ^ j p)

            If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative on all products of primes.

            theorem UniqueFactorizationMonoid.multiplicative_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] (f : αβ) (a : α) (b : α) (h0 : f 0 = 0) (h1 : ∀ {x y : α}, IsUnit yf (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ), Prime pf (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, IsRelPrime x yf (x * y) = f x * f y) :
            f (a * b) = f a * f b

            If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative everywhere.

            @[reducible, inline]

            FactorSet α representation elements of unique factorization domain as multisets. Multiset α produced by normalizedFactors are only unique up to associated elements, while the multisets in FactorSet α are unique by equality and restricted to irreducible elements. This gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete lattice structure. Infimum is the greatest common divisor and supremum is the least common multiple.

            Equations
            Instances For
              theorem Associates.FactorSet.coe_add {α : Type u_1} [CancelCommMonoidWithZero α] {a : Multiset { a : Associates α // Irreducible a }} {b : Multiset { a : Associates α // Irreducible a }} :
              (a + b) = a + b

              Evaluates the product of a FactorSet to be the product of the corresponding multiset, or 0 if there is none.

              Equations
              Instances For
                @[simp]
                theorem Associates.prod_top {α : Type u_1} [CancelCommMonoidWithZero α] :
                .prod = 0
                @[simp]
                theorem Associates.prod_coe {α : Type u_1} [CancelCommMonoidWithZero α] {s : Multiset { a : Associates α // Irreducible a }} :
                Associates.FactorSet.prod s = (Multiset.map Subtype.val s).prod
                @[simp]
                theorem Associates.prod_add {α : Type u_1} [CancelCommMonoidWithZero α] (a : Associates.FactorSet α) (b : Associates.FactorSet α) :
                (a + b).prod = a.prod * b.prod
                theorem Associates.prod_mono {α : Type u_1} [CancelCommMonoidWithZero α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} :
                a ba.prod b.prod

                bcount p s is the multiplicity of p in the FactorSet s (with bundled p)

                Equations
                Instances For

                  count p s is the multiplicity of the irreducible p in the FactorSet s.

                  If p is not irreducible, count p s is defined to be 0.

                  Equations
                  Instances For
                    @[simp]
                    theorem Associates.count_some {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : Irreducible p) (s : Multiset { a : Associates α // Irreducible a }) :
                    p.count s = Multiset.count p, hp s
                    @[simp]
                    theorem Associates.count_zero {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : Irreducible p) :
                    p.count 0 = 0

                    membership in a FactorSet (bundled version)

                    Equations
                    Instances For

                      FactorSetMem p s is the predicate that the irreducible p is a member of s : FactorSet α.

                      If p is not irreducible, p is not a member of any FactorSet.

                      Equations
                      Instances For
                        Equations
                        • Associates.instMembershipFactorSet = { mem := Associates.FactorSetMem }
                        @[simp]
                        theorem Associates.factorSetMem_eq_mem {α : Type u_1} [CancelCommMonoidWithZero α] (p : Associates α) (s : Associates.FactorSet α) :
                        p.FactorSetMem s = (p s)
                        theorem Associates.mem_factorSet_some {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {hp : Irreducible p} {l : Multiset { a : Associates α // Irreducible a }} :
                        p l p, hp l
                        theorem Associates.unique' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} :
                        (ap, Irreducible a)(aq, Irreducible a)p.prod = q.prodp = q
                        theorem Associates.prod_le_prod_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} (hp : ap, Irreducible a) (hq : aq, Irreducible a) :
                        p.prod q.prod p q
                        noncomputable def Associates.factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :

                        This returns the multiset of irreducible factors as a FactorSet, a multiset of irreducible associates WithTop.

                        Equations
                        Instances For

                          This returns the multiset of irreducible factors of an associate as a FactorSet, a multiset of irreducible associates WithTop.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[deprecated Associates.factors_zero]

                            Alias of Associates.factors_zero.

                            @[simp]
                            theorem Associates.factors_mk {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) (h : a 0) :
                            @[simp]
                            theorem Associates.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) :
                            a.factors.prod = a
                            @[deprecated Associates.factors_eq_top_iff_zero]

                            Alias of Associates.factors_eq_top_iff_zero.

                            theorem Associates.factors_eq_some_iff_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} :
                            (∃ (s : Multiset { p : Associates α // Irreducible p }), a.factors = s) a 0
                            theorem Associates.eq_of_factors_eq_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} (h : a.factors = b.factors) :
                            a = b
                            @[simp]
                            theorem Associates.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) (b : Associates α) :
                            (a * b).factors = a.factors + b.factors
                            theorem Associates.factors_mono {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} :
                            a ba.factors b.factors
                            @[simp]
                            theorem Associates.factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} :
                            a.factors b.factors a b
                            theorem Associates.eq_factors_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} {b : Associates α} (ha : a 0) (hb : b 0) (h : ∀ (p : Associates α), Irreducible pp.count a.factors = p.count b.factors) :
                            a.factors = b.factors
                            theorem Associates.eq_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} {b : Associates α} (ha : a 0) (hb : b 0) (h : ∀ (p : Associates α), Irreducible pp.count a.factors = p.count b.factors) :
                            a = b
                            theorem Associates.count_le_count_of_factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b 0) (hp : Irreducible p) (h : a.factors b.factors) :
                            p.count a.factors p.count b.factors
                            theorem Associates.count_le_count_of_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b 0) (hp : Irreducible p) (h : a b) :
                            p.count a.factors p.count b.factors
                            Equations
                            • Associates.instSup = { sup := fun (a b : Associates α) => (a.factors b.factors).prod }
                            Equations
                            • Associates.instInf = { inf := fun (a b : Associates α) => (a.factors b.factors).prod }
                            Equations
                            • Associates.instLattice = let __src := Associates.instPartialOrder; Lattice.mk
                            theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) (b : Associates α) :
                            (a b) * (a b) = a * b
                            theorem Associates.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {p : Associates α} (hm : p a.factors) :
                            p a
                            theorem Associates.dvd_of_mem_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : Associates α} {hp : Irreducible p} {hz : a 0} (h_mem : p, hp Associates.factors' a) :
                            theorem Associates.mem_factors'_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a 0) (hp : Irreducible p) (hd : p a) :
                            theorem Associates.mem_factors'_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a 0) (hp : Irreducible p) :
                            theorem Associates.mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a 0) (hp : Irreducible p) (hd : p a) :
                            theorem Associates.mem_factors_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a 0) (hp : Irreducible p) :
                            theorem Associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {b : α} (ha : a 0) (hb : b 0) (h : Associates.mk a Associates.mk b 1) :
                            ∃ (p : α), Prime p p a p b
                            theorem Associates.coprime_iff_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {b : α} (ha0 : a 0) (hb0 : b 0) :
                            Associates.mk a Associates.mk b = 1 ∀ {d : α}, d ad b¬Prime d
                            theorem Associates.factors_self {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates α} (hp : Irreducible p) :
                            p.factors = {p, hp}
                            theorem Associates.factors_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ) :
                            (p ^ k).factors = (Multiset.replicate k p, hp)
                            theorem Associates.prime_pow_le_iff_le_bcount {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] {m : Associates α} {p : Associates α} (h₁ : m 0) (h₂ : Irreducible p) {k : } :
                            p ^ k m k Associates.bcount p, h₂ m.factors
                            theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {m : Associates α} {p : Associates α} (h₁ : m 0) (h₂ : Irreducible p) {k : } :
                            p ^ k m k p.count m.factors
                            theorem Associates.le_of_count_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {m : Associates α} {p : Associates α} (h0 : m 0) (hp : Irreducible p) :
                            p.count m.factors 0p m
                            theorem Associates.count_ne_zero_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : α} {p : α} (ha0 : a 0) (hp : Irreducible p) :
                            (Associates.mk p).count (Associates.mk a).factors 0 p a
                            theorem Associates.count_self {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] [DecidableEq (Associates α)] {p : Associates α} (hp : Irreducible p) :
                            p.count p.factors = 1
                            theorem Associates.count_eq_zero_of_ne {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} {q : Associates α} (hp : Irreducible p) (hq : Irreducible q) (h : p q) :
                            p.count q.factors = 0
                            theorem Associates.count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} (ha : a 0) {b : Associates α} (hb : b 0) {p : Associates α} (hp : Irreducible p) :
                            p.count (a * b).factors = p.count a.factors + p.count b.factors
                            theorem Associates.count_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} (ha : a 0) {b : Associates α} (hb : b 0) (hab : ∀ (d : Associates α), d ad b¬Prime d) {p : Associates α} (hp : Irreducible p) :
                            p.count a.factors = 0 p.count b.factors = 0
                            theorem Associates.count_mul_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ad b¬Prime d) :
                            p.count a.factors = 0 p.count a.factors = p.count (a * b).factors
                            theorem Associates.count_mul_of_coprime' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ad b¬Prime d) :
                            p.count (a * b).factors = p.count a.factors p.count (a * b).factors = p.count b.factors
                            theorem Associates.dvd_count_of_dvd_count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ad b¬Prime d) {k : } (habk : k p.count (a * b).factors) :
                            k p.count a.factors
                            @[simp]
                            theorem Associates.pow_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a : Associates α} {k : } :
                            (a ^ k).factors = k a.factors
                            theorem Associates.count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] [DecidableEq (Associates α)] {a : Associates α} (ha : a 0) {p : Associates α} (hp : Irreducible p) (k : ) :
                            p.count (a ^ k).factors = k * p.count a.factors
                            theorem Associates.dvd_count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] [DecidableEq (Associates α)] {a : Associates α} (ha : a 0) {p : Associates α} (hp : Irreducible p) (k : ) :
                            k p.count (a ^ k).factors
                            theorem Associates.is_pow_of_dvd_count {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} (ha : a 0) {k : } (hk : ∀ (p : Associates α), Irreducible pk p.count a.factors) :
                            ∃ (b : Associates α), a = b ^ k
                            theorem Associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} {a : Associates α} (hp : Irreducible p) {n : } (h : a p ^ n) :
                            a = p ^ p.count a.factors

                            The only divisors of prime powers are prime powers. See eq_pow_find_of_dvd_irreducible_pow for an explicit expression as a p-power (without using count).

                            theorem Associates.count_factors_eq_find_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [(p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ) → Decidable (a p ^ n)] {n : } (h : a p ^ n) :
                            Nat.find = p.count a.factors
                            theorem Associates.eq_pow_of_mul_eq_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} {c : Associates α} (ha : a 0) (hb : b 0) (hab : ∀ (d : Associates α), d ad b¬Prime d) {k : } (h : a * b = c ^ k) :
                            ∃ (d : Associates α), a = d ^ k
                            theorem Associates.eq_pow_find_of_dvd_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ) → Decidable (a p ^ n)] {n : } (h : a p ^ n) :
                            a = p ^ Nat.find

                            The only divisors of prime powers are prime powers.

                            toGCDMonoid constructs a GCD monoid out of a unique factorization domain.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              toNormalizedGCDMonoid constructs a GCD monoid out of a normalization on a unique factorization domain.

                              Equations
                              Instances For
                                noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Fintype Mˣ] (y : M) (hy : y 0) :
                                Fintype { x : M // x y }

                                If y is a nonzero element of a unique factorization monoid with finitely many units (e.g. , Ideal (ring_of_integers K)), it has finitely many divisors.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  This returns the multiset of irreducible factors as a Finsupp.

                                  Equations
                                  Instances For
                                    @[simp]

                                    The support of factorization n is exactly the Finset of normalized factors

                                    @[simp]
                                    theorem factorization_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {a : α} {b : α} (ha : a 0) (hb : b 0) :

                                    For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

                                    For any p, the power of p in x^n is n times the power in x

                                    theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot {R : Type u_2} [CommSemiring R] [IsDomain R] [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ) :
                                    xI, Prime x

                                    Every non-zero prime ideal in a unique factorization domain contains a prime element.

                                    theorem induction_on_primes {P : Prop} (h₀ : P 0) (h₁ : P 1) (h : ∀ (p a : ), Nat.Prime pP aP (p * a)) (n : ) :
                                    P n