# mathlib3documentation

ring_theory.multiplicity

# Multiplicity of a divisor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 α] (a b : α) :

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

Equations
@[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
theorem multiplicity.finite_iff_dom {α : Type u_1} [monoid α] {a b : α} :
b).dom
theorem multiplicity.finite_def {α : Type u_1} [monoid α] {a b : α} :
(n : ), ¬a ^ (n + 1) b
theorem multiplicity.not_dvd_one_of_finite_one_right {α : Type u_1} [monoid α] {a : α} :
¬a 1
@[norm_cast]
theorem multiplicity.not_finite_iff_forall {α : Type u_1} [monoid α] {a b : α} :
(n : ), a ^ n b
theorem multiplicity.not_unit_of_finite {α : Type u_1} [monoid α] {a b : α} (h : b) :
theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [monoid α] {a b c : α} :
(b * c)
theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [monoid α] {a b : α} {k : } :
k b a ^ k b
theorem multiplicity.pow_multiplicity_dvd {α : Type u_1} [monoid α] {a b : α} (h : b) :
a ^ b).get h b
theorem multiplicity.is_greatest {α : Type u_1} [monoid α] {a b : α} {m : } (hm : b < m) :
¬a ^ m b
theorem multiplicity.is_greatest' {α : Type u_1} [monoid α] {a b : α} {m : } (h : b) (hm : b).get h < m) :
¬a ^ m b
theorem multiplicity.pos_of_dvd {α : Type u_1} [monoid α] {a b : α} (hfin : b) (hdiv : a b) :
0 < b).get hfin
theorem multiplicity.unique {α : Type u_1} [monoid α] {a b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
k = b
theorem multiplicity.unique' {α : Type u_1} [monoid α] {a b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
k = b).get _
theorem multiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [monoid α] {a b : α} {k : } (hk : a ^ k b) :
k b
theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [monoid α] {a b : α} {k : } :
a ^ k b k b
theorem multiplicity.multiplicity_lt_iff_neg_dvd {α : Type u_1} [monoid α] {a b : α} {k : } :
b < k ¬a ^ k b
theorem multiplicity.eq_coe_iff {α : Type u_1} [monoid α] {a b : α} {n : } :
b = n a ^ n b ¬a ^ (n + 1) b
theorem multiplicity.eq_top_iff {α : Type u_1} [monoid α] {a b : α} :
b = (n : ), a ^ n b
@[simp]
theorem multiplicity.is_unit_left {α : Type u_1} [monoid α] {a : α} (b : α) (ha : is_unit a) :
b =
@[simp]
theorem multiplicity.one_left {α : Type u_1} [monoid α] (b : α) :
b =
@[simp]
theorem multiplicity.get_one_right {α : Type u_1} [monoid α] {a : α} (ha : 1) :
1).get ha = 0
@[simp]
theorem multiplicity.unit_left {α : Type u_1} [monoid α] (a : α) (u : αˣ) :
theorem multiplicity.multiplicity_eq_zero {α : Type u_1} [monoid α] {a b : α} :
b = 0 ¬a b
theorem multiplicity.multiplicity_ne_zero {α : Type u_1} [monoid α] {a b : α} :
b 0 a b
theorem multiplicity.eq_top_iff_not_finite {α : Type u_1} [monoid α] {a b : α} :
b =
theorem multiplicity.ne_top_iff_finite {α : Type u_1} [monoid α] {a b : α} :
b
theorem multiplicity.lt_top_iff_finite {α : Type u_1} [monoid α] {a b : α} :
b <
theorem multiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [monoid α] {a b : α} (hfin : b) :
(c : α), b = a ^ b).get hfin * c ¬a c
theorem multiplicity.multiplicity_le_multiplicity_iff {α : Type u_1} [monoid α] {a b c d : α} :
b d (n : ), a ^ n b c ^ n d
theorem multiplicity.multiplicity_eq_multiplicity_iff {α : Type u_1} [monoid α] {a b c d : α} :
b = d (n : ), a ^ n b c ^ n d
theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right {α : Type u_1} [monoid α] {a b c : α} (h : b c) :
b c
theorem multiplicity.eq_of_associated_right {α : Type u_1} [monoid α] {a b c : α} (h : c) :
b = c
theorem multiplicity.dvd_of_multiplicity_pos {α : Type u_1} [monoid α] {a b : α} (h : 0 < b) :
a b
theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [monoid α] {a b : α} :
0 < b a b
theorem multiplicity.finite_nat_iff {a b : } :
a 1 0 < b
theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [monoid α] {a b : α} :
a b 0 < b

Alias of the reverse direction of multiplicity.dvd_iff_multiplicity_pos.

theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [comm_monoid α] {a b c : α} :
(b * c)
theorem multiplicity.is_unit_right {α : Type u_1} [comm_monoid α] {a b : α} (ha : ¬) (hb : is_unit b) :
b = 0
theorem multiplicity.one_right {α : Type u_1} [comm_monoid α] {a : α} (ha : ¬) :
1 = 0
theorem multiplicity.unit_right {α : Type u_1} [comm_monoid α] {a : α} (ha : ¬) (u : αˣ) :
= 0
theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left {α : Type u_1} [comm_monoid α] {a b c : α} (hdvd : a b) :
c c
theorem multiplicity.eq_of_associated_left {α : Type u_1} [comm_monoid α] {a b c : α} (h : b) :
c = c
theorem multiplicity.ne_zero_of_finite {α : Type u_1} {a b : α} (h : b) :
b 0
@[protected, simp]
theorem multiplicity.zero {α : Type u_1} (a : α) :
0 =
@[simp]
theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} (a : α) (ha : a 0) :
a = 0
theorem multiplicity.multiplicity_mk_eq_multiplicity {α : Type u_1} {a b : α} :
= b
theorem multiplicity.min_le_multiplicity_add {α : Type u_1} [semiring α] {p a b : α} :
b) (a + b)
@[protected, simp]
theorem multiplicity.neg {α : Type u_1} [ring α] (a b : α) :
(-b) = b
theorem multiplicity.int.nat_abs (a : ) (b : ) :
=
theorem multiplicity.multiplicity_add_of_gt {α : Type u_1} [ring α] {p a b : α} (h : b < a) :
(a + b) = b
theorem multiplicity.multiplicity_sub_of_gt {α : Type u_1} [ring α] {p a b : α} (h : b < a) :
(a - b) = b
theorem multiplicity.multiplicity_add_eq_min {α : Type u_1} [ring α] {p a b : α} (h : a b) :
(a + b) = b)
theorem multiplicity.finite_mul_aux {α : Type u_1} {p : α} (hp : prime p) {n m : } {a b : α} :
¬p ^ (n + 1) a ¬p ^ (m + 1) b ¬p ^ (n + m + 1) a * b
theorem multiplicity.finite_mul {α : Type u_1} {p a b : α} (hp : prime p) :
(a * b)
theorem multiplicity.finite_mul_iff {α : Type u_1} {p a b : α} (hp : prime p) :
(a * b)
theorem multiplicity.finite_pow {α : Type u_1} {p a : α} (hp : prime p) {k : } (ha : a) :
(a ^ k)
@[simp]
theorem multiplicity.multiplicity_self {α : Type u_1} {a : α} (ha : ¬) (ha0 : a 0) :
a = 1
@[simp]
theorem multiplicity.get_multiplicity_self {α : Type u_1} {a : α} (ha : a) :
a).get ha = 1
@[protected]
theorem multiplicity.mul' {α : Type u_1} {p a b : α} (hp : prime p) (h : (a * b)).dom) :
(a * b)).get h = a).get _ + b).get _
@[protected]
theorem multiplicity.mul {α : Type u_1} {p a b : α} (hp : prime p) :
(a * b) = a + b
theorem multiplicity.finset.prod {α : Type u_1} {β : Type u_2} {p : α} (hp : prime p) (s : finset β) (f : β α) :
(s.prod (λ (x : β), f x)) = s.sum (λ (x : β), (f x))
@[protected]
theorem multiplicity.pow' {α : Type u_1} {p a : α} (hp : prime p) (ha : a) {k : } :
(a ^ k)).get _ = k * a).get ha
theorem multiplicity.pow {α : Type u_1} {p a : α} (hp : prime p) {k : } :
(a ^ k) = k a
theorem multiplicity.multiplicity_pow_self {α : Type u_1} {p : α} (h0 : p 0) (hu : ¬) (n : ) :
(p ^ n) = n
theorem multiplicity.multiplicity_pow_self_of_prime {α : Type u_1} {p : α} (hp : prime p) (n : ) :
(p ^ n) = n
noncomputable def multiplicity.add_valuation {R : Type u_2} [comm_ring R] [is_domain R] {p : R} (hp : prime p) :

multiplicity of a prime inan integral domain as an additive valuation to part_enat.

Equations
• = multiplicity.add_valuation._proof_1 _ multiplicity.add_valuation._proof_3 _
@[simp]
theorem multiplicity.add_valuation_apply {R : Type u_2} [comm_ring R] [is_domain R] {p : R} {hp : prime p} {r : R} :
= r
theorem multiplicity_eq_zero_of_coprime {p a b : } (hp : p 1) (hle : a b) (hab : a.coprime b) :
a = 0