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 #

source
def multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (a b : α) :
enat

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

Equations
source
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
source
theorem multiplicity.finite_iff_dom {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity.finite a b ↔ (multiplicity a b).dom
source
theorem multiplicity.finite_def {α : Type u_1} [comm_monoid α] {a b : α} :
multiplicity.finite a b ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b
source
@[norm_cast]
theorem multiplicity.int.coe_nat_multiplicity (a b : ℕ) :
multiplicity ↑a ↑b = multiplicity a b
source
theorem multiplicity.not_finite_iff_forall {α : Type u_1} [comm_monoid α] {a b : α} :
¬multiplicity.finite a b ↔ ∀ (n : ℕ), a ^ n ∣ b
source
theorem multiplicity.not_unit_of_finite {α : Type u_1} [comm_monoid α] {a b : α} (h : multiplicity.finite a b) :
¬is_unit a
source
theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [comm_monoid α] {a b c : α} :
multiplicity.finite a (b * c) → multiplicity.finite a c
source
theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [comm_monoid α] {a b c : α} :
multiplicity.finite a (b * c) → multiplicity.finite a b
source
theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : ℕ} :
↑k ≤ multiplicity a b → a ^ k ∣ b
source
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
source
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
source
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
source
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
source
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
source
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 _
source
theorem multiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : ℕ} (hk : a ^ k ∣ b) :
↑k ≤ multiplicity a b
source
theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : ℕ} :
a ^ k ∣ b ↔ ↑k ≤ multiplicity a b
source
theorem multiplicity.multiplicity_lt_iff_neg_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : ℕ} :
multiplicity a b < ↑k ↔ ¬a ^ k ∣ b
source
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
source
theorem multiplicity.eq_top_iff {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity a b = ⊤ ↔ ∀ (n : ℕ), a ^ n ∣ b
source
@[simp]
theorem multiplicity.is_unit_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (b : α) (ha : is_unit a) :
multiplicity a b = ⊤
source
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
source
@[simp]
theorem multiplicity.one_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (b : α) :
multiplicity 1 b = ⊤
source
theorem multiplicity.one_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (ha : ¬is_unit a) :
multiplicity a 1 = 0
source
@[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
source
@[simp]
theorem multiplicity.unit_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (a : α) (u : αˣ) :
multiplicity ↑u a = ⊤
source
theorem multiplicity.unit_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a : α} (ha : ¬is_unit a) (u : αˣ) :
multiplicity a ↑u = 0
source
theorem multiplicity.multiplicity_eq_zero_of_not_dvd {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} (ha : ¬a ∣ b) :
multiplicity a b = 0
source
theorem multiplicity.eq_top_iff_not_finite {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity a b = ⊤ ↔ ¬multiplicity.finite a b
source
theorem multiplicity.ne_top_iff_finite {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity a b ≠ ⊤ ↔ multiplicity.finite a b
source
theorem multiplicity.lt_top_iff_finite {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
multiplicity a b < ⊤ ↔ multiplicity.finite a b
source
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
source
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 ∣ b → c ^ n ∣ d
source
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
source
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
source
theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b c : α} (h : b ∣ c) :
multiplicity a b ≤ multiplicity a c
source
theorem multiplicity.eq_of_associated_right {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b c : α} (h : associated b c) :
multiplicity a b = multiplicity a c
source
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
source
theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
0 < multiplicity a b ↔ a ∣ b
source
theorem multiplicity.finite_nat_iff {a b : ℕ} :
multiplicity.finite a b ↔ a ≠ 1 ∧ 0 < b
source
theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
a ∣ b → 0 < multiplicity a b

Alias of dvd_iff_multiplicity_pos.

source
theorem multiplicity.ne_zero_of_finite {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (h : multiplicity.finite a b) :
b ≠ 0
source
@[protected, simp]
theorem multiplicity.zero {α : Type u_1} [comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] (a : α) :
multiplicity a 0 = ⊤
source
@[simp]
theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] (a : α) (ha : a ≠ 0) :
multiplicity 0 a = 0
source
theorem multiplicity.min_le_multiplicity_add {α : Type u_1} [comm_semiring α] [decidable_rel has_dvd.dvd] {p a b : α} :
min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
source
@[protected, simp]
theorem multiplicity.neg {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] (a b : α) :
multiplicity a (-b) = multiplicity a b
source
theorem multiplicity.int.nat_abs (a : ℕ) (b : ℤ) :
multiplicity a b.nat_abs = multiplicity ↑a b
source
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) :
multiplicity p (a + b) = multiplicity p b
source
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) :
multiplicity p (a - b) = multiplicity p b
source
theorem multiplicity.multiplicity_add_eq_min {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] {p a b : α} (h : multiplicity p a ≠ multiplicity p b) :
multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
source
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
source
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)
source
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
source
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)
source
@[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
source
@[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
source
@[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 _
source
@[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
source
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 (∏ (x : β) in s, f x) = ∑ (x : β) in s, multiplicity p (f x)
source
@[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
source
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
source
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
source
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
source
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) :
add_valuation R enat

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

Equations
source
@[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
source
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
source
theorem multiplicity_eq_factorization {n p : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :
multiplicity p n = ↑(⇑(n.factorization) p)