mathlib documentation

ring_theory.multiplicity

theorem nat.find_le {p q : → Prop} [decidable_pred p] [decidable_pred q] (h : ∀ (n : ), q np n) (hp : ∃ (n : ), p n) (hq : ∃ (n : ), q n) :

def multiplicity {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] :
α → α → 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
def multiplicity.finite {α : Type u_1} [comm_monoid α] :
α → α → 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 : α} :

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 : } :
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) :
(multiplicity a b).get h < m¬a ^ m b

theorem multiplicity.unique {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} {k : } :
a ^ k b¬a ^ (k + 1) bk = multiplicity a 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 : } :
a ^ k bk multiplicity a 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_some_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

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

@[simp]
theorem multiplicity.one_left {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] (b : α) :

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.dvd_of_multiplicity_pos {α : Type u_1} [comm_monoid α] [decidable_rel has_dvd.dvd] {a b : α} :
0 < multiplicity a ba 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 multiplicity.ne_zero_of_finite {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :

@[simp]
theorem multiplicity.zero {α : Type u_1} [comm_monoid_with_zero α] [decidable_rel has_dvd.dvd] (a : α) :

@[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 : α} :

theorem multiplicity.multiplicity_sub_of_gt {α : Type u_1} [comm_ring α] [decidable_rel has_dvd.dvd] {p a b : α} :

theorem multiplicity.finite_mul_aux {α : Type u_1} [comm_cancel_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} [comm_cancel_monoid_with_zero α] {p a b : α} :

theorem multiplicity.finite_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] {p a : α} (hp : prime p) {k : } :

@[simp]
theorem multiplicity.multiplicity_self {α : Type u_1} [comm_cancel_monoid_with_zero α] [decidable_rel has_dvd.dvd] {a : α} :
¬is_unit aa 0multiplicity a a = 1

theorem multiplicity.mul' {α : Type u_1} [comm_cancel_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 _

theorem multiplicity.mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p a b : α} :

theorem multiplicity.finset.prod {α : Type u_1} [comm_cancel_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)

theorem multiplicity.pow' {α : Type u_1} [comm_cancel_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} [comm_cancel_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p a : α} (hp : prime p) {k : } :

theorem multiplicity.multiplicity_pow_self {α : Type u_1} [comm_cancel_monoid_with_zero α] [decidable_rel has_dvd.dvd] {p : α} (h0 : p 0) (hu : ¬is_unit p) (n : ) :
multiplicity p (p ^ n) = n

theorem multiplicity_eq_zero_of_coprime {p a b : } :
p 1multiplicity p a multiplicity p ba.coprime bmultiplicity p a = 0