# 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} [] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (b : α) :

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
Instances For
@[reducible, inline]
abbrev multiplicity.Finite {α : Type u_1} [] (a : α) (b : α) :

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

Equations
Instances For
theorem multiplicity.finite_iff_dom {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
().Dom
theorem multiplicity.finite_def {α : Type u_1} [] {a : α} {b : α} :
∃ (n : ), ¬a ^ (n + 1) b
theorem multiplicity.not_dvd_one_of_finite_one_right {α : Type u_1} [] {a : α} :
¬a 1
@[deprecated multiplicity.Int.natCast_multiplicity]

Alias of multiplicity.Int.natCast_multiplicity.

theorem multiplicity.not_finite_iff_forall {α : Type u_1} [] {a : α} {b : α} :
∀ (n : ), a ^ n b
theorem multiplicity.not_unit_of_finite {α : Type u_1} [] {a : α} {b : α} (h : ) :
theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [] {a : α} {b : α} {c : α} :
multiplicity.Finite a (b * c)
theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
k a ^ k b
theorem multiplicity.pow_multiplicity_dvd {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (h : ) :
a ^ ().get h b
theorem multiplicity.is_greatest {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {m : } (hm : < m) :
¬a ^ m b
theorem multiplicity.is_greatest' {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {m : } (h : ) (hm : ().get h < m) :
¬a ^ m b
theorem multiplicity.pos_of_dvd {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (hfin : ) (hdiv : a b) :
0 < ().get hfin
theorem multiplicity.unique {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
k =
theorem multiplicity.unique' {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
k = ().get
theorem multiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) :
k
theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
a ^ k b k
theorem multiplicity.multiplicity_lt_iff_not_dvd {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
< k ¬a ^ k b
theorem multiplicity.eq_coe_iff {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {n : } :
= n a ^ n b ¬a ^ (n + 1) b
theorem multiplicity.eq_top_iff {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
= ∀ (n : ), a ^ n b
@[simp]
theorem multiplicity.isUnit_left {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (b : α) (ha : ) :
theorem multiplicity.one_left {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] (b : α) :
@[simp]
theorem multiplicity.get_one_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ) :
().get ha = 0
theorem multiplicity.unit_left {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (u : αˣ) :
multiplicity (u) a =
theorem multiplicity.multiplicity_eq_zero {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
= 0 ¬a b
theorem multiplicity.multiplicity_ne_zero {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
0 a b
theorem multiplicity.eq_top_iff_not_finite {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
theorem multiplicity.ne_top_iff_finite {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
theorem multiplicity.lt_top_iff_finite {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
theorem multiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (hfin : ) :
∃ (c : α), b = a ^ ().get hfin * c ¬a c
theorem multiplicity.multiplicity_le_multiplicity_iff {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {a : α} {b : α} {c : β} {d : β} :
∀ (n : ), a ^ n bc ^ n d
theorem multiplicity.multiplicity_eq_multiplicity_iff {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {a : α} {b : α} {c : β} {d : β} :
= ∀ (n : ), a ^ n b c ^ n d
theorem multiplicity.le_multiplicity_map {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {F : Type u_3} [FunLike F α β] [] (f : F) {a : α} {b : α} :
multiplicity (f a) (f b)
theorem multiplicity.multiplicity_map_eq {α : Type u_1} {β : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {F : Type u_3} [EquivLike F α β] [] (f : F) {a : α} {b : α} :
multiplicity (f a) (f b) =
theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : b c) :
theorem multiplicity.eq_of_associated_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : ) :
=
theorem multiplicity.dvd_of_multiplicity_pos {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (h : 0 < ) :
a b
theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
0 < a b
theorem multiplicity.finite_nat_iff {a : } {b : } :
a 1 0 < b
theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
a b0 <

Alias of the reverse direction of multiplicity.dvd_iff_multiplicity_pos.

theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [] {a : α} {b : α} {c : α} :
multiplicity.Finite a (b * c)
theorem multiplicity.isUnit_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (ha : ¬) (hb : ) :
= 0
theorem multiplicity.one_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬) :
= 0
theorem multiplicity.unit_right {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬) (u : αˣ) :
multiplicity a u = 0
theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (hdvd : a b) :
theorem multiplicity.eq_of_associated_left {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : ) :
=
theorem multiplicity.ne_zero_of_finite {α : Type u_1} [] {a : α} {b : α} (h : ) :
b 0
@[simp]
theorem multiplicity.zero {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) :
@[simp]
theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (ha : a 0) :
= 0
theorem multiplicity.multiplicity_mk_eq_multiplicity {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : ) => x x_1] {a : α} {b : α} :
=
theorem multiplicity.min_le_multiplicity_add {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} :
min () () multiplicity p (a + b)
@[simp]
theorem multiplicity.neg {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (b : α) :
theorem multiplicity.Int.natAbs (a : ) (b : ) :
multiplicity a b.natAbs = 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 (a + 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 (a - 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 + b) = min () ()
theorem multiplicity.finite_mul_aux {α : Type u_1} {p : α} (hp : ) {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} {p : α} {a : α} {b : α} (hp : ) :
multiplicity.Finite p (a * b)
theorem multiplicity.finite_mul_iff {α : Type u_1} {p : α} {a : α} {b : α} (hp : ) :
theorem multiplicity.finite_pow {α : Type u_1} {p : α} {a : α} (hp : ) {k : } :
multiplicity.Finite p (a ^ k)
@[simp]
theorem multiplicity.multiplicity_self {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬) (ha0 : a 0) :
= 1
@[simp]
theorem multiplicity.get_multiplicity_self {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ) :
().get ha = 1
theorem multiplicity.mul' {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (hp : ) (h : (multiplicity p (a * b)).Dom) :
(multiplicity p (a * b)).get h = ().get + ().get
theorem multiplicity.mul {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (hp : ) :
multiplicity p (a * b) = +
theorem multiplicity.Finset.prod {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {β : Type u_3} {p : α} (hp : ) (s : ) (f : βα) :
multiplicity p (s.prod fun (x : β) => f x) = s.sum fun (x : β) => multiplicity p (f x)
theorem multiplicity.pow' {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} (hp : ) (ha : ) {k : } :
(multiplicity p (a ^ k)).get = k * ().get ha
theorem multiplicity.pow {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} (hp : ) {k : } :
multiplicity p (a ^ k) = k
theorem multiplicity.multiplicity_pow_self {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} (h0 : p 0) (hu : ¬) (n : ) :
multiplicity p (p ^ n) = n
theorem multiplicity.multiplicity_pow_self_of_prime {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] {p : α} (hp : ) (n : ) :
multiplicity p (p ^ n) = n
theorem multiplicity_eq_zero_of_coprime {p : } {a : } {b : } (hp : p 1) (hle : ) (hab : a.Coprime b) :
= 0
theorem multiplicity.finite_int_iff {a : } {b : } :
a.natAbs 1 b 0
instance multiplicity.decidableNat :
DecidableRel fun (a b : ) => ().Dom
Equations
instance multiplicity.decidableInt :
DecidableRel fun (a b : ) => ().Dom
Equations