mathlib documentation

ring_theory.multiplicity

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 #

def multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (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} [comm_monoid α] (a b : α) :
Prop

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

Equations
theorem multiplicity.finite_def {α : Type u_1} [comm_monoid α] {a b : α} :
multiplicity.finite a b ∃ (n : ), ¬a ^ (n + 1) b
theorem multiplicity.not_finite_iff_forall {α : Type u_1} [comm_monoid α] {a b : α} :
¬multiplicity.finite a b ∀ (n : ), a ^ n b
theorem multiplicity.not_unit_of_finite {α : Type u_1} [comm_monoid α] {a b : α} (h : multiplicity.finite a b) :
theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [comm_monoid α] {a b c : α} :
theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [comm_monoid α] {a b c : α} :
theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } :
k multiplicity a ba ^ k b
theorem multiplicity.pow_multiplicity_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (h : multiplicity.finite a b) :
a ^ (multiplicity a b).get h b
theorem multiplicity.is_greatest {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {m : } (hm : multiplicity a b < m) :
¬a ^ m b
theorem multiplicity.is_greatest' {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {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} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (hfin : multiplicity.finite a b) (hdiv : a b) :
0 < (multiplicity a b).get hfin
theorem multiplicity.unique {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
theorem multiplicity.unique' {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {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} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } (hk : a ^ k b) :
theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } :
theorem multiplicity.multiplicity_lt_iff_neg_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } :
theorem multiplicity.eq_coe_iff {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {n : } :
multiplicity a b = n a ^ n b ¬a ^ (n + 1) b
theorem multiplicity.eq_top_iff {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity a b = ∀ (n : ), a ^ n b
@[simp]
theorem multiplicity.is_unit_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (b : α) (ha : is_unit a) :
theorem multiplicity.is_unit_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (ha : ¬is_unit a) (hb : is_unit b) :
@[simp]
theorem multiplicity.one_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (b : α) :
theorem multiplicity.one_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (ha : ¬is_unit a) :
@[simp]
theorem multiplicity.get_one_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (ha : multiplicity.finite a 1) :
(multiplicity a 1).get ha = 0
@[simp]
theorem multiplicity.unit_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (a : α) (u : αˣ) :
theorem multiplicity.unit_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (ha : ¬is_unit a) (u : αˣ) :
theorem multiplicity.multiplicity_eq_zero_of_not_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (ha : ¬a b) :
theorem multiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {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} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b c d : α} :
multiplicity a b multiplicity c d ∀ (n : ), a ^ n bc ^ n d
theorem multiplicity.eq_of_associated_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b c : α} (h : associated a b) :
theorem multiplicity.eq_of_associated_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b c : α} (h : associated b c) :
theorem multiplicity.dvd_of_multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (h : 0 < multiplicity a b) :
a b
theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
0 < multiplicity a b a b
theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
a b0 < multiplicity a b

Alias of the reverse direction of multiplicity.dvd_iff_multiplicity_pos.

theorem multiplicity.ne_zero_of_finite {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (h : multiplicity.finite a b) :
b 0
@[protected, simp]
theorem multiplicity.zero {α : Type u_1} [comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] (a : α) :
@[protected, simp]
theorem multiplicity.neg {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] (a b : α) :
theorem multiplicity.multiplicity_add_of_gt {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] {p a b : α} (h : multiplicity p b < multiplicity p a) :
theorem multiplicity.multiplicity_sub_of_gt {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] {p a b : α} (h : multiplicity p b < multiplicity p a) :
theorem multiplicity.finite_mul_aux {α : Type u_1} [cancel_comm_monoid_with_zero α] {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} [cancel_comm_monoid_with_zero α] {p a b : α} (hp : prime p) :
theorem multiplicity.finite_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] {p a : α} (hp : prime p) {k : } (ha : multiplicity.finite p a) :
@[simp]
theorem multiplicity.multiplicity_self {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {a : α} (ha : ¬is_unit a) (ha0 : a 0) :
@[protected]
theorem multiplicity.mul' {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {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 _
@[protected]
theorem multiplicity.mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p a b : α} (hp : prime p) :
theorem multiplicity.finset.prod {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {β : Type u_2} {p : α} (hp : prime p) (s : finset β) (f : β → α) :
multiplicity p (s.prod (λ (x : β), f x)) = s.sum (λ (x : β), multiplicity p (f x))
@[protected]
theorem multiplicity.pow' {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {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} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p a : α} (hp : prime p) {k : } :
theorem multiplicity.multiplicity_pow_self {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p : α} (h0 : p 0) (hu : ¬is_unit p) (n : ) :
multiplicity p (p ^ n) = n
noncomputable def multiplicity.add_valuation {R : Type u_2} [comm_ring R] [is_domain R] {p : R} [decidable_rel has_dvd.dvd] (hp : prime p) :

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

Equations
@[simp]
theorem multiplicity.add_valuation_apply {R : Type u_2} [comm_ring R] [is_domain R] {p : R} [decidable_rel has_dvd.dvd] {hp : prime p} {r : R} :
theorem multiplicity_eq_zero_of_coprime {p a b : } (hp : p 1) (hle : multiplicity p a multiplicity p b) (hab : a.coprime b) :