Documentation

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Set of factors #

Main definitions #

TODO #

@[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 b : Multiset { a : Associates α // Irreducible a }} :
      ↑(a + b) = a + b
      theorem Associates.FactorSet.sup_add_inf_eq_add {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (a b : FactorSet α) :
      ab + ab = 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_add {α : Type u_1} [CancelCommMonoidWithZero α] (a b : FactorSet α) :
          (a + b).prod = a.prod * b.prod
          theorem Associates.prod_mono {α : Type u_1} [CancelCommMonoidWithZero α] {a b : 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_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
                          @[simp]
                          @[deprecated Associates.reducible_notMem_factorSet (since := "2025-05-23")]

                          Alias of Associates.reducible_notMem_factorSet.

                          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
                                Instances For
                                  @[simp]
                                  theorem Associates.eq_factors_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b : Associates α} (ha : a 0) (hb : b 0) (h : ∀ (p : Associates α), Irreducible pp.count a.factors = p.count b.factors) :
                                  theorem Associates.eq_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b : Associates α} (ha : a 0) (hb : b 0) (h : ∀ (p : Associates α), Irreducible pp.count a.factors = p.count b.factors) :
                                  a = b
                                  Equations
                                    Equations
                                      theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a b : Associates α) :
                                      (ab) * (ab) = a * b
                                      theorem Associates.dvd_of_mem_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : Associates α} {hp : Irreducible p} {hz : a 0} (h_mem : p, hp 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.exists_prime_dvd_of_not_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (ha : a 0) (hb : b 0) (h : Associates.mk aAssociates.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 aAssociates.mk b = 1 ∀ {d : α}, d ad b¬Prime d
                                      theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {m p : Associates α} (h₁ : m 0) (h₂ : Irreducible p) {k : } :
                                      p ^ k m k p.count m.factors
                                      theorem Associates.count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} (ha : a 0) {b : Associates α} (hb : b 0) {p : Associates α} (hp : Irreducible p) :
                                      theorem Associates.count_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} (ha : a 0) {b : Associates α} (hb : b 0) (hab : ∀ (d : Associates α), d ad b¬Prime d) {p : Associates α} (hp : Irreducible p) :
                                      theorem Associates.count_mul_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b : Associates α} (hb : b 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ad b¬Prime d) :
                                      theorem Associates.count_mul_of_coprime' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ad b¬Prime d) :
                                      theorem Associates.dvd_count_of_dvd_count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a 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) :
                                      theorem Associates.count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] {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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] {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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} (ha : a 0) {k : } (hk : ∀ (p : Associates α), Irreducible pk p.count a.factors) :
                                      ∃ (b : Associates α), a = b ^ k

                                      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.eq_pow_of_mul_eq_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b 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 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.