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 elementsa
andb
of a commutative monoid returns the largest numbern
such thata ^ n ∣ b
or infinity, written⊤
, ifa ^ n ∣ b
for all natural numbersn
.multiplicity.Finite a b
: a predicate denoting that the multiplicity ofa
inb
is finite.
def
multiplicity
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
(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
- multiplicity a b = PartENat.find fun (n : ℕ) => ¬a ^ (n + 1) ∣ b
Instances For
@[reducible, inline]
multiplicity.Finite a b
indicates that the multiplicity of a
in b
is finite.
Instances For
theorem
multiplicity.finite_iff_dom
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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
theorem
multiplicity.Int.natCast_multiplicity
(a : ℕ)
(b : ℕ)
:
multiplicity ↑a ↑b = multiplicity a b
@[deprecated multiplicity.Int.natCast_multiplicity]
theorem
multiplicity.Int.coe_nat_multiplicity
(a : ℕ)
(b : ℕ)
:
multiplicity ↑a ↑b = multiplicity a b
Alias of multiplicity.Int.natCast_multiplicity
.
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 α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{k : ℕ}
:
↑k ≤ multiplicity a b → a ^ k ∣ b
theorem
multiplicity.pow_multiplicity_dvd
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
(h : multiplicity.Finite a b)
:
a ^ (multiplicity a b).get h ∣ b
theorem
multiplicity.is_greatest
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{m : ℕ}
(hm : multiplicity a b < ↑m)
:
theorem
multiplicity.is_greatest'
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{m : ℕ}
(h : multiplicity.Finite a b)
(hm : (multiplicity a b).get h < m)
:
theorem
multiplicity.pos_of_dvd
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{k : ℕ}
(hk : a ^ k ∣ b)
:
↑k ≤ multiplicity a b
theorem
multiplicity.pow_dvd_iff_le_multiplicity
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{k : ℕ}
:
a ^ k ∣ b ↔ ↑k ≤ multiplicity a b
theorem
multiplicity.multiplicity_lt_iff_not_dvd
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{k : ℕ}
:
theorem
multiplicity.eq_top_iff
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
@[simp]
theorem
multiplicity.isUnit_left
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
(b : α)
(ha : IsUnit a)
:
multiplicity a b = ⊤
theorem
multiplicity.one_left
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
(b : α)
:
multiplicity 1 b = ⊤
@[simp]
theorem
multiplicity.get_one_right
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
(ha : multiplicity.Finite a 1)
:
(multiplicity a 1).get ha = 0
theorem
multiplicity.unit_left
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
(a : α)
(u : αˣ)
:
multiplicity (↑u) a = ⊤
theorem
multiplicity.multiplicity_eq_zero
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity a b = 0 ↔ ¬a ∣ b
theorem
multiplicity.multiplicity_ne_zero
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity a b ≠ 0 ↔ a ∣ b
theorem
multiplicity.eq_top_iff_not_finite
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity a b = ⊤ ↔ ¬multiplicity.Finite a b
theorem
multiplicity.ne_top_iff_finite
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity a b ≠ ⊤ ↔ multiplicity.Finite a b
theorem
multiplicity.lt_top_iff_finite
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity a b < ⊤ ↔ multiplicity.Finite a b
theorem
multiplicity.exists_eq_pow_mul_and_not_dvd
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
(hfin : multiplicity.Finite a b)
:
theorem
multiplicity.multiplicity_le_multiplicity_iff
{α : Type u_1}
{β : Type u_2}
[Monoid α]
[Monoid β]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
[DecidableRel fun (x1 x2 : β) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
[DecidableRel fun (x1 x2 : β) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
[DecidableRel fun (x1 x2 : β) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
[DecidableRel fun (x1 x2 : β) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{c : α}
(h : b ∣ c)
:
multiplicity a b ≤ multiplicity a c
theorem
multiplicity.eq_of_associated_right
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
(h : 0 < multiplicity a b)
:
a ∣ b
theorem
multiplicity.dvd_iff_multiplicity_pos
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
:
0 < multiplicity a b ↔ a ∣ b
theorem
has_dvd.dvd.multiplicity_pos
{α : Type u_1}
[Monoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
(ha : ¬IsUnit a)
(hb : IsUnit b)
:
multiplicity a b = 0
theorem
multiplicity.one_right
{α : Type u_1}
[CommMonoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
(ha : ¬IsUnit a)
:
multiplicity a 1 = 0
theorem
multiplicity.unit_right
{α : Type u_1}
[CommMonoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
(ha : ¬IsUnit a)
(u : αˣ)
:
multiplicity a ↑u = 0
theorem
multiplicity.multiplicity_le_multiplicity_of_dvd_left
{α : Type u_1}
[CommMonoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
{b : α}
{c : α}
(hdvd : a ∣ b)
:
multiplicity b c ≤ multiplicity a c
theorem
multiplicity.eq_of_associated_left
{α : Type u_1}
[CommMonoid α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
(a : α)
:
multiplicity a 0 = ⊤
@[simp]
theorem
multiplicity.multiplicity_zero_eq_zero_of_ne_zero
{α : Type u_1}
[MonoidWithZero α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
(a : α)
(ha : a ≠ 0)
:
multiplicity 0 a = 0
theorem
multiplicity.multiplicity_mk_eq_multiplicity
{α : Type u_1}
[CommMonoidWithZero α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
[DecidableRel fun (x1 x2 : Associates α) => x1 ∣ x2]
{a : α}
{b : α}
:
multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
theorem
multiplicity.min_le_multiplicity_add
{α : Type u_1}
[Semiring α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{p : α}
{a : α}
{b : α}
:
min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
@[simp]
theorem
multiplicity.neg
{α : Type u_1}
[Ring α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
(a : α)
(b : α)
:
multiplicity a (-b) = multiplicity a b
theorem
multiplicity.multiplicity_add_of_gt
{α : Type u_1}
[Ring α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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
{α : 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 (x1 x2 : α) => x1 ∣ x2]
{a : α}
(ha : ¬IsUnit a)
(ha0 : a ≠ 0)
:
multiplicity a a = 1
@[simp]
theorem
multiplicity.get_multiplicity_self
{α : Type u_1}
[CancelCommMonoidWithZero α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{a : α}
(ha : multiplicity.Finite a a)
:
(multiplicity a a).get ha = 1
theorem
multiplicity.mul'
{α : Type u_1}
[CancelCommMonoidWithZero α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{β : Type u_3}
{p : α}
(hp : Prime p)
(s : Finset β)
(f : β → α)
:
multiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, multiplicity p (f x)
theorem
multiplicity.pow'
{α : Type u_1}
[CancelCommMonoidWithZero α]
[DecidableRel fun (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 (x1 x2 : α) => x1 ∣ x2]
{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 : a.Coprime b)
:
multiplicity p a = 0
theorem
multiplicity.finite_int_iff_natAbs_finite
{a : ℤ}
{b : ℤ}
:
multiplicity.Finite a b ↔ multiplicity.Finite a.natAbs b.natAbs
Equations
- multiplicity.decidableNat x✝ x = decidable_of_iff (x✝ ≠ 1 ∧ 0 < x) ⋯
Equations
- multiplicity.decidableInt x✝ x = decidable_of_iff (x✝.natAbs ≠ 1 ∧ x ≠ 0) ⋯