Multiplicity of a divisor

For a commutative monoid, this file introduces the notion of multiplicity of a divisor and proves several basic results on it.

Main definitions

• multiplicity a b: for two elements a and b of a commutative monoid returns the largest number n such that a ^ n ∣ b or infinity, written ⊤, if a ^ n ∣ b for all natural numbers n.
• multiplicity.Finite a b: a predicate denoting that the multiplicity of a in b is finite.

def multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (a : α) (b : α) : PartENat

multiplicity a b returns the largest natural number n such that a ^ n ∣ b, as a PartENat or natural with infinity. If ∀ n, a ^ n ∣ b, then it returns ⊤

Equations

• multiplicity a b = PartENat.find fun (n : ℕ) => ¬a ^ (n + 1) ∣ b

@[reducible]

def multiplicity.Finite {α : Type u_1} [Monoid α] (a : α) (b : α) : Prop

multiplicity.Finite a b indicates that the multiplicity of a in b is finite.

Equations

• multiplicity.Finite a b = ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

theorem multiplicity.finite_iff_dom {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity.Finite a b ↔ (multiplicity a b).Dom

theorem multiplicity.finite_def {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity.Finite a b ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

theorem multiplicity.not_dvd_one_of_finite_one_right {α : Type u_1} [Monoid α] {a : α} : multiplicity.Finite a 1 → ¬a ∣ 1

theorem multiplicity.Int.coe_nat_multiplicity (a : ℕ) (b : ℕ) : multiplicity ↑a ↑b = multiplicity a b

theorem multiplicity.not_finite_iff_forall {α : Type u_1} [Monoid α] {a : α} {b : α} : ¬multiplicity.Finite a b ↔ ∀ (n : ℕ), a ^ n ∣ b

theorem multiplicity.not_unit_of_finite {α : Type u_1} [Monoid α] {a : α} {b : α} (h : multiplicity.Finite a b) : ¬IsUnit a

theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} : multiplicity.Finite a (b * c) → multiplicity.Finite a b

theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} : ↑k ≤ multiplicity a b → a ^ k ∣ b

theorem multiplicity.pow_multiplicity_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} (h : multiplicity.Finite a b) : a ^ (multiplicity a b).get h ∣ b

theorem multiplicity.is_greatest {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {m : ℕ} (hm : multiplicity a b < ↑m) : ¬a ^ m ∣ b

theorem multiplicity.is_greatest' {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {m : ℕ} (h : multiplicity.Finite a b) (hm : (multiplicity a b).get h < m) : ¬a ^ m ∣ b

theorem multiplicity.pos_of_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} (hfin : multiplicity.Finite a b) (hdiv : a ∣ b) : 0 < (multiplicity a b).get hfin

theorem multiplicity.unique {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : ↑k = multiplicity a b

theorem multiplicity.unique' {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : k = (multiplicity a b).get ⋯

theorem multiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) : ↑k ≤ multiplicity a b

theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} : a ^ k ∣ b ↔ ↑k ≤ multiplicity a b

theorem multiplicity.multiplicity_lt_iff_not_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {k : ℕ} : multiplicity a b < ↑k ↔ ¬a ^ k ∣ b

theorem multiplicity.eq_coe_iff {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {n : ℕ} : multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

theorem multiplicity.eq_top_iff {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b = ⊤ ↔ ∀ (n : ℕ), a ^ n ∣ b

@[simp]

theorem multiplicity.isUnit_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (b : α) (ha : IsUnit a) : multiplicity a b = ⊤

theorem multiplicity.one_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (b : α) : multiplicity 1 b = ⊤

@[simp]

theorem multiplicity.get_one_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (ha : multiplicity.Finite a 1) : (multiplicity a 1).get ha = 0

theorem multiplicity.unit_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (a : α) (u : αˣ) : multiplicity (↑u) a = ⊤

theorem multiplicity.multiplicity_eq_zero {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b = 0 ↔ ¬a ∣ b

theorem multiplicity.multiplicity_ne_zero {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b ≠ 0 ↔ a ∣ b

theorem multiplicity.eq_top_iff_not_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b = ⊤ ↔ ¬multiplicity.Finite a b

theorem multiplicity.ne_top_iff_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b ≠ ⊤ ↔ multiplicity.Finite a b

theorem multiplicity.lt_top_iff_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : multiplicity a b < ⊤ ↔ multiplicity.Finite a b

theorem multiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} (hfin : multiplicity.Finite a b) : ∃ (c : α), b = a ^ (multiplicity a b).get hfin * c ∧ ¬a ∣ c

theorem multiplicity.multiplicity_le_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : β) => x ∣ x_1] {a : α} {b : α} {c : β} {d : β} : multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

theorem multiplicity.multiplicity_eq_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : β) => x ∣ x_1] {a : α} {b : α} {c : β} {d : β} : multiplicity a b = multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b ↔ c ^ n ∣ d

theorem multiplicity.le_multiplicity_map {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : β) => x ∣ x_1] {F : Type u_3} [FunLike F α β] [MonoidHomClass F α β] (f : F) {a : α} {b : α} : multiplicity a b ≤ multiplicity (f a) (f b)

theorem multiplicity.multiplicity_map_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : β) => x ∣ x_1] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a : α} {b : α} : multiplicity (f a) (f b) = multiplicity a b

theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {c : α} (h : b ∣ c) : multiplicity a b ≤ multiplicity a c

theorem multiplicity.eq_of_associated_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {c : α} (h : Associated b c) : multiplicity a b = multiplicity a c

theorem multiplicity.dvd_of_multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} (h : 0 < multiplicity a b) : a ∣ b

theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : 0 < multiplicity a b ↔ a ∣ b

theorem multiplicity.finite_nat_iff {a : ℕ} {b : ℕ} : multiplicity.Finite a b ↔ a ≠ 1 ∧ 0 < b

theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} : a ∣ b → 0 < multiplicity a b

Alias of the reverse direction of multiplicity.dvd_iff_multiplicity_pos.

theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} : multiplicity.Finite a (b * c) → multiplicity.Finite a c

theorem multiplicity.isUnit_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : multiplicity a b = 0

theorem multiplicity.one_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (ha : ¬IsUnit a) : multiplicity a 1 = 0

theorem multiplicity.unit_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (ha : ¬IsUnit a) (u : αˣ) : multiplicity a ↑u = 0

theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {c : α} (hdvd : a ∣ b) : multiplicity b c ≤ multiplicity a c

theorem multiplicity.eq_of_associated_left {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} {b : α} {c : α} (h : Associated a b) : multiplicity b c = multiplicity a c

theorem multiplicity.ne_zero_of_finite {α : Type u_1} [MonoidWithZero α] {a : α} {b : α} (h : multiplicity.Finite a b) : b ≠ 0

@[simp]

theorem multiplicity.zero {α : Type u_1} [MonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (a : α) : multiplicity a 0 = ⊤

@[simp]

theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (a : α) (ha : a ≠ 0) : multiplicity 0 a = 0

theorem multiplicity.multiplicity_mk_eq_multiplicity {α : Type u_1} [CommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : Associates α) => x ∣ x_1] {a : α} {b : α} : multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b

theorem multiplicity.min_le_multiplicity_add {α : Type u_1} [Semiring α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} : min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)

@[simp]

theorem multiplicity.neg {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] (a : α) (b : α) : multiplicity a (-b) = multiplicity a b

theorem multiplicity.Int.natAbs (a : ℕ) (b : ℤ) : multiplicity a (Int.natAbs b) = multiplicity (↑a) b

theorem multiplicity.multiplicity_add_of_gt {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} (h : multiplicity p b < multiplicity p a) : multiplicity p (a + b) = multiplicity p b

theorem multiplicity.multiplicity_sub_of_gt {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} (h : multiplicity p b < multiplicity p a) : multiplicity p (a - b) = multiplicity p b

theorem multiplicity.multiplicity_add_eq_min {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} (h : multiplicity p a ≠ multiplicity p b) : multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

theorem multiplicity.finite_mul_aux {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} {n : ℕ} {m : ℕ} : ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b

theorem multiplicity.finite_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} (hp : Prime p) : multiplicity.Finite p a → multiplicity.Finite p b → multiplicity.Finite p (a * b)

theorem multiplicity.finite_mul_iff {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} (hp : Prime p) : multiplicity.Finite p (a * b) ↔ multiplicity.Finite p a ∧ multiplicity.Finite p b

theorem multiplicity.finite_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} (hp : Prime p) {k : ℕ} : multiplicity.Finite p a → multiplicity.Finite p (a ^ k)

@[simp]

theorem multiplicity.multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) : multiplicity a a = 1

@[simp]

theorem multiplicity.get_multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {a : α} (ha : multiplicity.Finite a a) : (multiplicity a a).get ha = 1

theorem multiplicity.mul' {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} (hp : Prime p) (h : (multiplicity p (a * b)).Dom) : (multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯

theorem multiplicity.mul {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} {b : α} (hp : Prime p) : multiplicity p (a * b) = multiplicity p a + multiplicity p b

theorem multiplicity.Finset.prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {β : Type u_3} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) : multiplicity p (Finset.prod s fun (x : β) => f x) = Finset.sum s fun (x : β) => multiplicity p (f x)

theorem multiplicity.pow' {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} (hp : Prime p) (ha : multiplicity.Finite p a) {k : ℕ} : (multiplicity p (a ^ k)).get ⋯ = k * (multiplicity p a).get ha

theorem multiplicity.pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} {a : α} (hp : Prime p) {k : ℕ} : multiplicity p (a ^ k) = k • multiplicity p a

theorem multiplicity.multiplicity_pow_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : multiplicity p (p ^ n) = ↑n

theorem multiplicity.multiplicity_pow_self_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] {p : α} (hp : Prime p) (n : ℕ) : multiplicity p (p ^ n) = ↑n

theorem multiplicity_eq_zero_of_coprime {p : ℕ} {a : ℕ} {b : ℕ} (hp : p ≠ 1) (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.Coprime a b) : multiplicity p a = 0