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

• emultiplicity a b: for two elements a and b of a commutative monoid returns the largest number n such that a ^ n ∣ b or infinity, written ⊤, if a ^ n ∣ b for all natural numbers n.
• multiplicity a b: a ℕ-valued version of multiplicity, defaulting for 1 instead of ⊤. The reason for using 1 as a default value instead of 0 is to have multiplicity_eq_zero_iff.
• multiplicity.Finite a b: a predicate denoting that the multiplicity of a in b is finite.

@[reducible, inline]

abbrev multiplicity.Finite {α : Type u_1} [Monoid α] (a : α) (b : α) : Prop

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

Equations

• multiplicity.Finite a b = ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

noncomputable def emultiplicity {α : Type u_1} [Monoid α] (a : α) (b : α) : ℕ∞

emultiplicity a b returns the largest natural number n such that a ^ n ∣ b, as an ℕ∞. If ∀ n, a ^ n ∣ b then it returns ⊤.

Equations

• emultiplicity a b = if h : multiplicity.Finite a b then ↑(Nat.find h) else ⊤

noncomputable def multiplicity {α : Type u_1} [Monoid α] (a : α) (b : α) : ℕ

A ℕ-valued version of emultiplicity, returning 1 instead of ⊤.

Equations

• multiplicity a b = WithTop.untop' 1 (emultiplicity a b)

@[simp]

theorem emultiplicity_eq_top {α : Type u_1} [Monoid α] {a : α} {b : α} : emultiplicity a b = ⊤ ↔ ¬multiplicity.Finite a b

theorem emultiplicity_lt_top {α : Type u_1} [Monoid α] {a : α} {b : α} : emultiplicity a b < ⊤ ↔ multiplicity.Finite a b

theorem finite_iff_emultiplicity_ne_top {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity.Finite a b ↔ emultiplicity a b ≠ ⊤

theorem Finite.emultiplicity_ne_top {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity.Finite a b → emultiplicity a b ≠ ⊤

Alias of the forward direction of finite_iff_emultiplicity_ne_top.

theorem finite_of_emultiplicity_eq_natCast {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : emultiplicity a b = ↑n) : multiplicity.Finite a b

theorem multiplicity_eq_of_emultiplicity_eq_some {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : emultiplicity a b = ↑n) : multiplicity a b = n

theorem emultiplicity_ne_of_multiplicity_ne {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} : multiplicity a b ≠ n → emultiplicity a b ≠ ↑n

theorem multiplicity.Finite.emultiplicity_eq_multiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} (h : multiplicity.Finite a b) : emultiplicity a b = ↑(multiplicity a b)

theorem multiplicity.Finite.emultiplicity_eq_iff_multiplicity_eq {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : multiplicity.Finite a b) : emultiplicity a b = ↑n ↔ multiplicity a b = n

theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_one {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : n ≠ 1) : emultiplicity a b = ↑n ↔ multiplicity a b = n

theorem emultiplicity_eq_zero_iff_multiplicity_eq_zero {α : Type u_1} [Monoid α] {a : α} {b : α} : emultiplicity a b = 0 ↔ multiplicity a b = 0

@[simp]

theorem multiplicity_eq_one_of_not_finite {α : Type u_1} [Monoid α] {a : α} {b : α} (h : ¬multiplicity.Finite a b) : multiplicity a b = 1

@[simp]

theorem multiplicity_le_emultiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} : ↑(multiplicity a b) ≤ emultiplicity a b

@[simp]

theorem multiplicity_eq_of_emultiplicity_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a : α} {b : α} {c : β} {d : β} (h : emultiplicity a b = emultiplicity c d) : multiplicity a b = multiplicity c d

theorem multiplicity_le_of_emultiplicity_le {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : emultiplicity a b ≤ ↑n) : multiplicity a b ≤ n

theorem multiplicity.Finite.emultiplicity_le_of_multiplicity_le {α : Type u_1} [Monoid α] {a : α} {b : α} (hfin : multiplicity.Finite a b) {n : ℕ} (h : multiplicity a b ≤ n) : emultiplicity a b ≤ ↑n

theorem le_emultiplicity_of_le_multiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : n ≤ multiplicity a b) : ↑n ≤ emultiplicity a b

theorem multiplicity.Finite.le_multiplicity_of_le_emultiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} (hfin : multiplicity.Finite a b) {n : ℕ} (h : ↑n ≤ emultiplicity a b) : n ≤ multiplicity a b

theorem multiplicity_lt_of_emultiplicity_lt {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : emultiplicity a b < ↑n) : multiplicity a b < n

theorem multiplicity.Finite.emultiplicity_lt_of_multiplicity_lt {α : Type u_1} [Monoid α] {a : α} {b : α} (hfin : multiplicity.Finite a b) {n : ℕ} (h : multiplicity a b < n) : emultiplicity a b < ↑n

theorem lt_emultiplicity_of_lt_multiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} (h : n < multiplicity a b) : ↑n < emultiplicity a b

theorem multiplicity.Finite.lt_multiplicity_of_lt_emultiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} (hfin : multiplicity.Finite a b) {n : ℕ} (h : ↑n < emultiplicity a b) : n < multiplicity a b

theorem emultiplicity_pos_iff {α : Type u_1} [Monoid α] {a : α} {b : α} : 0 < emultiplicity a b ↔ 0 < multiplicity a b

theorem multiplicity.Finite.def {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity.Finite a b ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

theorem multiplicity.Finite.not_dvd_of_one_right {α : Type u_1} [Monoid α] {a : α} : multiplicity.Finite a 1 → ¬a ∣ 1

theorem Int.natCast_emultiplicity (a : ℕ) (b : ℕ) : emultiplicity ↑a ↑b = emultiplicity a b

theorem Int.natCast_multiplicity (a : ℕ) (b : ℕ) : multiplicity ↑a ↑b = multiplicity a b

@[deprecated Int.natCast_multiplicity]

theorem Int.coe_nat_multiplicity (a : ℕ) (b : ℕ) : multiplicity ↑a ↑b = multiplicity a b

Alias of Int.natCast_multiplicity.

theorem multiplicity.Finite.not_iff_forall {α : Type u_1} [Monoid α] {a : α} {b : α} : ¬multiplicity.Finite a b ↔ ∀ (n : ℕ), a ^ n ∣ b

theorem multiplicity.Finite.not_unit {α : Type u_1} [Monoid α] {a : α} {b : α} (h : multiplicity.Finite a b) : ¬IsUnit a

theorem multiplicity.Finite.mul_left {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} : multiplicity.Finite a (b * c) → multiplicity.Finite a b

theorem pow_dvd_of_le_emultiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hk : ↑k ≤ emultiplicity a b) : a ^ k ∣ b

theorem pow_dvd_of_le_multiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hk : k ≤ multiplicity a b) : a ^ k ∣ b

@[simp]

theorem pow_multiplicity_dvd {α : Type u_1} [Monoid α] (a : α) (b : α) : a ^ multiplicity a b ∣ b

theorem not_pow_dvd_of_emultiplicity_lt {α : Type u_1} [Monoid α] {a : α} {b : α} {m : ℕ} (hm : emultiplicity a b < ↑m) : ¬a ^ m ∣ b

theorem multiplicity.Finite.not_pow_dvd_of_multiplicity_lt {α : Type u_1} [Monoid α] {a : α} {b : α} (hf : multiplicity.Finite a b) {m : ℕ} (hm : multiplicity a b < m) : ¬a ^ m ∣ b

theorem multiplicity_pos_of_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} (hdiv : a ∣ b) : 0 < multiplicity a b

theorem emultiplicity_pos_of_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} (hdiv : a ∣ b) : 0 < emultiplicity a b

theorem emultiplicity_eq_of_dvd_of_not_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : emultiplicity a b = ↑k

theorem multiplicity_eq_of_dvd_of_not_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : multiplicity a b = k

theorem le_emultiplicity_of_pow_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hk : a ^ k ∣ b) : ↑k ≤ emultiplicity a b

theorem multiplicity.Finite.le_multiplicity_of_pow_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} (hf : multiplicity.Finite a b) {k : ℕ} (hk : a ^ k ∣ b) : k ≤ multiplicity a b

theorem pow_dvd_iff_le_emultiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} : a ^ k ∣ b ↔ ↑k ≤ emultiplicity a b

theorem multiplicity.Finite.pow_dvd_iff_le_multiplicity {α : Type u_1} [Monoid α] {a : α} {b : α} (hf : multiplicity.Finite a b) {k : ℕ} : a ^ k ∣ b ↔ k ≤ multiplicity a b

theorem emultiplicity_lt_iff_not_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} : emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b

theorem multiplicity.Finite.multiplicity_lt_iff_not_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} {k : ℕ} (hf : multiplicity.Finite a b) : multiplicity a b < k ↔ ¬a ^ k ∣ b

theorem emultiplicity_eq_coe {α : Type u_1} [Monoid α] {a : α} {b : α} {n : ℕ} : emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

theorem multiplicity.Finite.multiplicity_eq_iff {α : Type u_1} [Monoid α] {a : α} {b : α} (hf : multiplicity.Finite a b) {n : ℕ} : multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

@[simp]

theorem multiplicity.Finite.not_of_isUnit_left {α : Type u_1} [Monoid α] {a : α} (b : α) (ha : IsUnit a) : ¬multiplicity.Finite a b

theorem multiplicity.Finite.not_of_one_left {α : Type u_1} [Monoid α] (b : α) : ¬multiplicity.Finite 1 b

@[simp]

theorem emultiplicity_one_left {α : Type u_1} [Monoid α] (b : α) : emultiplicity 1 b = ⊤

@[simp]

theorem multiplicity.Finite.one_right {α : Type u_1} [Monoid α] {a : α} (ha : multiplicity.Finite a 1) : multiplicity a 1 = 0

theorem multiplicity.Finite.not_of_unit_left {α : Type u_1} [Monoid α] (a : α) (u : αˣ) : ¬multiplicity.Finite (↑u) a

theorem emultiplicity_eq_zero {α : Type u_1} [Monoid α] {a : α} {b : α} : emultiplicity a b = 0 ↔ ¬a ∣ b

theorem multiplicity_eq_zero {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity a b = 0 ↔ ¬a ∣ b

theorem emultiplicity_ne_zero {α : Type u_1} [Monoid α] {a : α} {b : α} : emultiplicity a b ≠ 0 ↔ a ∣ b

theorem multiplicity_ne_zero {α : Type u_1} [Monoid α] {a : α} {b : α} : multiplicity a b ≠ 0 ↔ a ∣ b

theorem multiplicity.Finite.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [Monoid α] {a : α} {b : α} (hfin : multiplicity.Finite a b) : ∃ (c : α), b = a ^ multiplicity a b * c ∧ ¬a ∣ c

theorem emultiplicity_le_emultiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a : α} {b : α} {c : β} {d : β} : emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

theorem multiplicity.Finite.multiplicity_le_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a : α} {b : α} {c : β} {d : β} (hab : multiplicity.Finite a b) (hcd : multiplicity.Finite c d) : multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

theorem emultiplicity_eq_emultiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a : α} {b : α} {c : β} {d : β} : emultiplicity a b = emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b ↔ c ^ n ∣ d

theorem le_emultiplicity_map {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {F : Type u_3} [FunLike F α β] [MonoidHomClass F α β] (f : F) {a : α} {b : α} : emultiplicity a b ≤ emultiplicity (f a) (f b)

theorem emultiplicity_map_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a : α} {b : α} : emultiplicity (f a) (f b) = emultiplicity a b

theorem multiplicity_map_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a : α} {b : α} : multiplicity (f a) (f b) = multiplicity a b

theorem emultiplicity_le_emultiplicity_of_dvd_right {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} (h : b ∣ c) : emultiplicity a b ≤ emultiplicity a c

theorem emultiplicity_eq_of_associated_right {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} (h : Associated b c) : emultiplicity a b = emultiplicity a c

theorem multiplicity_eq_of_associated_right {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} (h : Associated b c) : multiplicity a b = multiplicity a c

theorem dvd_of_emultiplicity_pos {α : Type u_1} [Monoid α] {a : α} {b : α} (h : 0 < emultiplicity a b) : a ∣ b

theorem dvd_of_multiplicity_pos {α : Type u_1} [Monoid α] {a : α} {b : α} (h : 0 < multiplicity a b) : a ∣ b

theorem dvd_iff_multiplicity_pos {α : Type u_1} [Monoid α] {a : α} {b : α} : 0 < multiplicity a b ↔ a ∣ b

theorem dvd_iff_emultiplicity_pos {α : Type u_1} [Monoid α] {a : α} {b : α} : 0 < emultiplicity a b ↔ a ∣ b

theorem Nat.multiplicity_finite_iff {a : ℕ} {b : ℕ} : multiplicity.Finite a b ↔ a ≠ 1 ∧ 0 < b

theorem Dvd.multiplicity_pos {α : Type u_1} [Monoid α] {a : α} {b : α} : a ∣ b → 0 < multiplicity a b

Alias of the reverse direction of dvd_iff_multiplicity_pos.

theorem multiplicity.Finite.mul_right {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} (hf : multiplicity.Finite a (b * c)) : multiplicity.Finite a c

theorem emultiplicity_of_isUnit_right {α : Type u_1} [CommMonoid α] {a : α} {b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : emultiplicity a b = 0

theorem multiplicity_of_isUnit_right {α : Type u_1} [CommMonoid α] {a : α} {b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : multiplicity a b = 0

theorem emultiplicity_of_one_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) : emultiplicity a 1 = 0

theorem multiplicity_of_one_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) : multiplicity a 1 = 0

theorem emultiplicity_of_unit_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) (u : αˣ) : emultiplicity a ↑u = 0

theorem multiplicity_of_unit_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) (u : αˣ) : multiplicity a ↑u = 0

theorem emultiplicity_le_emultiplicity_of_dvd_left {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} (hdvd : a ∣ b) : emultiplicity b c ≤ emultiplicity a c

theorem emultiplicity_eq_of_associated_left {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} (h : Associated a b) : emultiplicity b c = emultiplicity a c

theorem multiplicity_eq_of_associated_left {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} (h : Associated a b) : multiplicity b c = multiplicity a c

theorem emultiplicity_mk_eq_emultiplicity {α : Type u_1} [CommMonoid α] {a : α} {b : α} : emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

theorem multiplicity.Finite.ne_zero {α : Type u_1} [MonoidWithZero α] {a : α} {b : α} (h : multiplicity.Finite a b) : b ≠ 0

@[simp]

theorem emultiplicity_zero {α : Type u_1} [MonoidWithZero α] (a : α) : emultiplicity a 0 = ⊤

@[simp]

theorem emultiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] (a : α) (ha : a ≠ 0) : emultiplicity 0 a = 0

@[simp]

theorem multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] (a : α) (ha : a ≠ 0) : multiplicity 0 a = 0

theorem multiplicity.Finite.or_of_add {α : Type u_1} [Semiring α] {p : α} {a : α} {b : α} (hf : multiplicity.Finite p (a + b)) : multiplicity.Finite p a ∨ multiplicity.Finite p b

theorem min_le_emultiplicity_add {α : Type u_1} [Semiring α] {p : α} {a : α} {b : α} : emultiplicity p a ⊓ emultiplicity p b ≤ emultiplicity p (a + b)

@[simp]

theorem multiplicity.Finite.neg_iff {α : Type u_1} [Ring α] {a : α} {b : α} : multiplicity.Finite a (-b) ↔ multiplicity.Finite a b

theorem multiplicity.Finite.neg {α : Type u_1} [Ring α] {a : α} {b : α} : multiplicity.Finite a b → multiplicity.Finite a (-b)

Alias of the reverse direction of multiplicity.Finite.neg_iff.

@[simp]

theorem emultiplicity_neg {α : Type u_1} [Ring α] (a : α) (b : α) : emultiplicity a (-b) = emultiplicity a b

@[simp]

theorem multiplicity_neg {α : Type u_1} [Ring α] (a : α) (b : α) : multiplicity a (-b) = multiplicity a b

theorem Int.emultiplicity_natAbs (a : ℕ) (b : ℤ) : emultiplicity a b.natAbs = emultiplicity (↑a) b

theorem Int.multiplicity_natAbs (a : ℕ) (b : ℤ) : multiplicity a b.natAbs = multiplicity (↑a) b

theorem emultiplicity_add_of_gt {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (h : emultiplicity p b < emultiplicity p a) : emultiplicity p (a + b) = emultiplicity p b

theorem multiplicity.Finite.multiplicity_add_of_gt {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (hf : multiplicity.Finite p b) (h : multiplicity p b < multiplicity p a) : multiplicity p (a + b) = multiplicity p b

theorem emultiplicity_sub_of_gt {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (h : emultiplicity p b < emultiplicity p a) : emultiplicity p (a - b) = emultiplicity p b

theorem multiplicity_sub_of_gt {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (h : multiplicity p b < multiplicity p a) (hfin : multiplicity.Finite p b) : multiplicity p (a - b) = multiplicity p b

theorem emultiplicity_add_eq_min {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (h : emultiplicity p a ≠ emultiplicity p b) : emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

theorem multiplicity_add_eq_min {α : Type u_1} [Ring α] {p : α} {a : α} {b : α} (ha : multiplicity.Finite p a) (hb : multiplicity.Finite p b) (h : multiplicity p a ≠ multiplicity p b) : multiplicity p (a + b) = multiplicity p a ⊓ multiplicity p b

@[irreducible]

theorem multiplicity.finite_mul_aux {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} {n : ℕ} {m : ℕ} : ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b

theorem Prime.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) (hfin : multiplicity.Finite p a) {k : ℕ} : multiplicity.Finite p (a ^ k)

@[simp]

theorem multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} : multiplicity a a = 1

@[simp]

theorem multiplicity.Finite.emultiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} (hfin : multiplicity.Finite a a) : emultiplicity a a = 1

theorem multiplicity_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} (hp : Prime p) (hfin : multiplicity.Finite p (a * b)) : multiplicity p (a * b) = multiplicity p a + multiplicity p b

theorem emultiplicity_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} (hp : Prime p) : emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

theorem Finset.emultiplicity_prod {α : Type u_1} [CancelCommMonoidWithZero α] {β : Type u_3} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

theorem emultiplicity_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} (hp : Prime p) {k : ℕ} : emultiplicity p (a ^ k) = ↑k * emultiplicity p a

theorem multiplicity.Finite.multiplicity_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} (hp : Prime p) (ha : multiplicity.Finite p a) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a

theorem emultiplicity_pow_self {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : emultiplicity p (p ^ n) = ↑n

theorem multiplicity_pow_self {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : multiplicity p (p ^ n) = n

theorem emultiplicity_pow_self_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) (n : ℕ) : emultiplicity p (p ^ n) = ↑n

theorem multiplicity_pow_self_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] {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 Int.multiplicity_finite_iff_natAbs_finite {a : ℤ} {b : ℤ} : multiplicity.Finite a b ↔ multiplicity.Finite a.natAbs b.natAbs

theorem Int.multiplicity_finite_iff {a : ℤ} {b : ℤ} : multiplicity.Finite a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

instance Nat.decidableMultiplicityFinite : DecidableRel fun (a b : ℕ) => multiplicity.Finite a b

Equations

• x✝.decidableMultiplicityFinite x = decidable_of_iff' (x✝ ≠ 1 ∧ 0 < x) ⋯

instance Int.decidableMultiplicityFinite : DecidableRel fun (a b : ℤ) => multiplicity.Finite a b

Equations

• x✝.decidableMultiplicityFinite x = decidable_of_iff' (x✝.natAbs ≠ 1 ∧ x ≠ 0) ⋯