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 elementsaandbof a commutative monoid returns the largest numbernsuch thata ^ n ∣ bor infinity, written⊤, ifa ^ n ∣ bfor all natural numbersn.multiplicity.finite a b: a predicate denoting that the multiplicity ofainbis finite.
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
- multiplicity a b = part_enat.find (λ (n : ℕ), ¬a ^ (n + 1) ∣ b)
@[reducible]
multiplicity.finite a b indicates that the multiplicity of a in b is finite.
theorem
multiplicity.finite_iff_dom
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity.finite a b ↔ (multiplicity a b).dom
theorem
multiplicity.not_dvd_one_of_finite_one_right
{α : Type u_1}
[monoid α]
{a : α} :
multiplicity.finite a 1 → ¬a ∣ 1
@[norm_cast]
theorem
multiplicity.not_unit_of_finite
{α : Type u_1}
[monoid α]
{a b : α}
(h : multiplicity.finite a b) :
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 α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ} :
theorem
multiplicity.pow_multiplicity_dvd
{α : Type u_1}
[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}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{m : ℕ}
(hm : multiplicity a b < ↑m) :
theorem
multiplicity.is_greatest'
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{m : ℕ}
(h : multiplicity.finite a b)
(hm : (multiplicity a b).get h < m) :
theorem
multiplicity.pos_of_dvd
{α : Type u_1}
[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}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(hk : a ^ k ∣ b)
(hsucc : ¬a ^ (k + 1) ∣ b) :
↑k = multiplicity a b
theorem
multiplicity.unique'
{α : Type u_1}
[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}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ}
(hk : a ^ k ∣ b) :
↑k ≤ multiplicity a b
theorem
multiplicity.pow_dvd_iff_le_multiplicity
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ} :
theorem
multiplicity.multiplicity_lt_iff_neg_dvd
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{k : ℕ} :
theorem
multiplicity.eq_coe_iff
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
{n : ℕ} :
@[simp]
theorem
multiplicity.is_unit_left
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(b : α)
(ha : is_unit a) :
multiplicity a b = ⊤
@[simp]
theorem
multiplicity.one_left
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
(b : α) :
multiplicity 1 b = ⊤
@[simp]
theorem
multiplicity.get_one_right
{α : Type u_1}
[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}
[monoid α]
[decidable_rel has_dvd.dvd]
(a : α)
(u : αˣ) :
multiplicity ↑u a = ⊤
theorem
multiplicity.multiplicity_eq_zero
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b = 0 ↔ ¬a ∣ b
theorem
multiplicity.multiplicity_ne_zero
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b ≠ 0 ↔ a ∣ b
theorem
multiplicity.eq_top_iff_not_finite
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b = ⊤ ↔ ¬multiplicity.finite a b
theorem
multiplicity.ne_top_iff_finite
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b ≠ ⊤ ↔ multiplicity.finite a b
theorem
multiplicity.lt_top_iff_finite
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity a b < ⊤ ↔ multiplicity.finite a b
theorem
multiplicity.exists_eq_pow_mul_and_not_dvd
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
(hfin : multiplicity.finite a b) :
theorem
multiplicity.multiplicity_le_multiplicity_iff
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b c d : α} :
theorem
multiplicity.multiplicity_eq_multiplicity_iff
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b c d : α} :
theorem
multiplicity.multiplicity_le_multiplicity_of_dvd_right
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b c : α}
(h : b ∣ c) :
multiplicity a b ≤ multiplicity a c
theorem
multiplicity.eq_of_associated_right
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b c : α}
(h : associated b c) :
multiplicity a b = multiplicity a c
theorem
multiplicity.dvd_of_multiplicity_pos
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α}
(h : 0 < multiplicity a b) :
a ∣ b
theorem
multiplicity.dvd_iff_multiplicity_pos
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{a b : α} :
0 < multiplicity a b ↔ a ∣ b
theorem
has_dvd.dvd.multiplicity_pos
{α : Type u_1}
[monoid α]
[decidable_rel has_dvd.dvd]
{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}
[comm_monoid α]
{a b c : α} :
multiplicity.finite a (b * c) → multiplicity.finite a c
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) :
multiplicity a b = 0
theorem
multiplicity.one_right
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : ¬is_unit a) :
multiplicity a 1 = 0
theorem
multiplicity.unit_right
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : ¬is_unit a)
(u : αˣ) :
multiplicity a ↑u = 0
theorem
multiplicity.multiplicity_le_multiplicity_of_dvd_left
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b c : α}
(hdvd : a ∣ b) :
multiplicity b c ≤ multiplicity a c
theorem
multiplicity.eq_of_associated_left
{α : Type u_1}
[comm_monoid α]
[decidable_rel has_dvd.dvd]
{a b c : α}
(h : associated a b) :
multiplicity b c = multiplicity a c
theorem
multiplicity.ne_zero_of_finite
{α : Type u_1}
[monoid_with_zero α]
{a b : α}
(h : multiplicity.finite a b) :
b ≠ 0
@[protected, simp]
theorem
multiplicity.zero
{α : Type u_1}
[monoid_with_zero α]
[decidable_rel has_dvd.dvd]
(a : α) :
multiplicity a 0 = ⊤
@[simp]
theorem
multiplicity.multiplicity_zero_eq_zero_of_ne_zero
{α : Type u_1}
[monoid_with_zero α]
[decidable_rel has_dvd.dvd]
(a : α)
(ha : a ≠ 0) :
multiplicity 0 a = 0
theorem
multiplicity.multiplicity_mk_eq_multiplicity
{α : Type u_1}
[comm_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
[decidable_rel has_dvd.dvd]
{a b : α} :
multiplicity (associates.mk a) (associates.mk b) = multiplicity a b
theorem
multiplicity.min_le_multiplicity_add
{α : Type u_1}
[semiring α]
[decidable_rel has_dvd.dvd]
{p a b : α} :
linear_order.min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
@[protected, simp]
theorem
multiplicity.neg
{α : Type u_1}
[ring α]
[decidable_rel has_dvd.dvd]
(a b : α) :
multiplicity a (-b) = multiplicity a b
theorem
multiplicity.multiplicity_add_of_gt
{α : Type u_1}
[ring α]
[decidable_rel has_dvd.dvd]
{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 α]
[decidable_rel has_dvd.dvd]
{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 α]
[decidable_rel has_dvd.dvd]
{p a b : α}
(h : multiplicity p a ≠ multiplicity p b) :
multiplicity p (a + b) = linear_order.min (multiplicity p a) (multiplicity p b)
theorem
multiplicity.finite_mul
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
{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}
[cancel_comm_monoid_with_zero α]
{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}
[cancel_comm_monoid_with_zero α]
{p a : α}
(hp : prime p)
{k : ℕ}
(ha : multiplicity.finite p a) :
multiplicity.finite p (a ^ k)
@[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) :
multiplicity a a = 1
@[simp]
theorem
multiplicity.get_multiplicity_self
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{a : α}
(ha : multiplicity.finite a a) :
(multiplicity a a).get ha = 1
@[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) :
multiplicity p (a * b) = multiplicity p a + multiplicity p b
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 : ℕ} :
multiplicity p (a ^ k) = k • multiplicity p a
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
theorem
multiplicity.multiplicity_pow_self_of_prime
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_rel has_dvd.dvd]
{p : α}
(hp : prime 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
- multiplicity.add_valuation hp = add_valuation.of (multiplicity p) 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}
[decidable_rel has_dvd.dvd]
{hp : prime p}
{r : R} :
⇑(multiplicity.add_valuation hp) r = multiplicity p r
theorem
multiplicity_eq_zero_of_coprime
{p a b : ℕ}
(hp : p ≠ 1)
(hle : multiplicity p a ≤ multiplicity p b)
(hab : a.coprime b) :
multiplicity p a = 0