Set of factors

Main definitions

• Associates.FactorSet: multiset of factors of an element, unique up to propositional equality.
• Associates.factors: determine the FactorSet for a given element.

TODO

• set up the complete lattice structure on FactorSet.

@[reducible, inline]

abbrev Associates.FactorSet (α : Type u) [CancelCommMonoidWithZero α] : Type u

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

• Associates.FactorSet α = WithTop (Multiset { a : Associates α // Irreducible a })

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 α) : a ⊔ b + a ⊓ b = a + b

def Associates.FactorSet.prod {α : Type u_1} [CancelCommMonoidWithZero α] : FactorSet α → Associates α

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

Equations

• Associates.FactorSet.prod none = 0
• Associates.FactorSet.prod (some s) = (Multiset.map Subtype.val s).prod

@[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 }} : FactorSet.prod ↑s = (Multiset.map Subtype.val s).prod

@[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 ≤ b → a.prod ≤ b.prod

theorem Associates.FactorSet.prod_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (p : FactorSet α) : p.prod = 0 ↔ p = ⊤

def Associates.bcount {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (p : { a : Associates α // Irreducible a }) : FactorSet α → ℕ

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

Equations

• Associates.bcount p none = 0
• Associates.bcount p (some s) = Multiset.count p s

def Associates.count {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] (p : Associates α) : FactorSet α → ℕ

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

• p.count = if hp : Irreducible p then Associates.bcount ⟨p, hp⟩ else 0

@[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

theorem Associates.count_reducible {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : ¬Irreducible p) : p.count = 0

def Associates.BfactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] : { a : Associates α // Irreducible a } → FactorSet α → Prop

membership in a FactorSet (bundled version)

Equations

• Associates.BfactorSetMem x✝ none = True
• Associates.BfactorSetMem x✝ (some l) = (x✝ ∈ l)

def Associates.FactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] (s : FactorSet α) (p : Associates α) : Prop

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

• Associates.FactorSetMem s p = if hp : Irreducible p then Associates.BfactorSetMem ⟨p, hp⟩ s else False

instance Associates.instMembershipFactorSet {α : Type u_1} [CancelCommMonoidWithZero α] : Membership (Associates α) (FactorSet α)

Equations

• Associates.instMembershipFactorSet = { mem := Associates.FactorSetMem }

@[simp]

theorem Associates.factorSetMem_eq_mem {α : Type u_1} [CancelCommMonoidWithZero α] (p : Associates α) (s : FactorSet α) : FactorSetMem s p = (p ∈ s)

theorem Associates.mem_factorSet_top {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {hp : Irreducible p} : p ∈ ⊤

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.reducible_not_mem_factorSet {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} (hp : ¬Irreducible p) (s : FactorSet α) : p ∉ s

theorem Associates.irreducible_of_mem_factorSet {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {s : FactorSet α} (h : p ∈ s) : Irreducible p

theorem Associates.FactorSet.unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p q : FactorSet α} (h : p.prod = q.prod) : p = q

noncomputable def Associates.factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) : Multiset { a : Associates α // Irreducible a }

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

Equations

• Associates.factors' a = Multiset.pmap (fun (a : α) (ha : Irreducible a) => ⟨Associates.mk a, ⋯⟩) (UniqueFactorizationMonoid.factors a) ⋯

@[simp]

theorem Associates.map_subtype_coe_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} : Multiset.map Subtype.val (factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)

theorem Associates.factors'_cong {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : factors' a = factors' b

noncomputable def Associates.factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) : FactorSet α

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.

@[simp]

theorem Associates.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : factors 0 = ⊤

@[simp]

theorem Associates.factors_mk {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) (h : a ≠ 0) : (Associates.mk a).factors = ↑(factors' a)

@[simp]

theorem Associates.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) : a.factors.prod = a

@[simp]

theorem Associates.prod_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] (s : FactorSet α) : s.prod.factors = s

theorem Associates.factors_subsingleton {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Subsingleton α] {a : Associates α} : a.factors = ⊤

theorem Associates.factors_eq_top_iff_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} : a.factors = ⊤ ↔ a = 0

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 b : Associates α} (h : a.factors = b.factors) : a = b

theorem Associates.eq_of_prod_eq_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a b : FactorSet α} (h : a.prod = b.prod) : a = b

@[simp]

theorem Associates.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a b : Associates α) : (a * b).factors = a.factors + b.factors

theorem Associates.factors_mono {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : Associates α} : a ≤ b → a.factors ≤ b.factors

@[simp]

theorem Associates.factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a 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 b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → p.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 b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → p.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 b 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 b p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : a ≤ b) : p.count a.factors ≤ p.count b.factors

theorem Associates.prod_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a b : FactorSet α} : a.prod ≤ b.prod ↔ a ≤ b

noncomputable instance Associates.instMax {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : Max (Associates α)

Equations

• Associates.instMax = { max := fun (a b : Associates α) => (a.factors ⊔ b.factors).prod }

noncomputable instance Associates.instMin {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : Min (Associates α)

Equations

• Associates.instMin = { min := fun (a b : Associates α) => (a.factors ⊓ b.factors).prod }

noncomputable instance Associates.instLattice {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : Lattice (Associates α)

Equations

• Associates.instLattice = Lattice.mk (fun (x1 x2 : Associates α) => x1 ⊓ x2) ⋯ ⋯ ⋯

theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a b : Associates α) : (a ⊔ b) * (a ⊓ b) = a * b

theorem Associates.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a 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⟩ ∈ factors' a) : p ∣ Associates.mk a

theorem Associates.mem_factors'_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) : ⟨Associates.mk p, ⋯⟩ ∈ factors' a

theorem Associates.mem_factors'_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : ⟨Associates.mk p, ⋯⟩ ∈ factors' a ↔ p ∣ a

theorem Associates.mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) : Associates.mk p ∈ (Associates.mk a).factors

theorem Associates.mem_factors_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : Associates.mk p ∈ (Associates.mk a).factors ↔ 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 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 ∣ a → d ∣ 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 p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} : p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors

@[simp]

theorem Associates.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] : factors 1 = 0

@[simp]

theorem Associates.pow_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a : Associates α} {k : ℕ} : (a ^ k).factors = k • a.factors

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.le_of_count_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {m p : Associates α} (h0 : m ≠ 0) (hp : Irreducible p) : p.count m.factors ≠ 0 → p ≤ 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) : p.count p.factors = 1

theorem Associates.count_eq_zero_of_ne {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (habk : k ∣ p.count (a * b).factors) : k ∣ p.count a.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 p → k ∣ p.count a.factors) : ∃ (b : Associates α), a = b ^ k

theorem Associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p 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 α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a 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 b c : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ 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.