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 0 instead of ⊤.

@[reducible, inline]

abbrev FiniteMultiplicity {α : Type u_1} [Monoid α] (a b : α) : Prop

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

Equations

• FiniteMultiplicity 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 : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤

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

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

Equations

• multiplicity a b = (emultiplicity a b).toNat

@[simp]

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

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

theorem finiteMultiplicity_iff_emultiplicity_ne_top {α : Type u_1} [Monoid α] {a b : α} : FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

theorem finiteMultiplicity_of_emultiplicity_eq_natCast {α : Type u_1} [Monoid α] {a b : α} {n : ℕ} (h : emultiplicity a b = ↑n) : FiniteMultiplicity 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 FiniteMultiplicity.emultiplicity_eq_multiplicity {α : Type u_1} [Monoid α] {a b : α} (h : FiniteMultiplicity a b) : emultiplicity a b = ↑(multiplicity a b)

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

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

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

@[deprecated emultiplicity_eq_iff_multiplicity_eq_of_ne_zero (since := "2026-09-08")]

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

Alias of emultiplicity_eq_iff_multiplicity_eq_of_ne_zero.

@[simp]

theorem multiplicity_eq_zero_of_not_finiteMultiplicity {α : Type u_1} [Monoid α] {a b : α} (h : ¬FiniteMultiplicity a b) : multiplicity a b = 0

@[deprecated multiplicity_eq_zero_of_not_finiteMultiplicity (since := "2026-09-08")]

theorem multiplicity_eq_one_of_not_finiteMultiplicity {α : Type u_1} [Monoid α] {a b : α} (h : ¬FiniteMultiplicity a b) : multiplicity a b = 0

Alias of multiplicity_eq_zero_of_not_finiteMultiplicity.

@[simp]

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

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 FiniteMultiplicity.emultiplicity_le_of_multiplicity_le {α : Type u_1} [Monoid α] {a b : α} (hfin : FiniteMultiplicity 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 FiniteMultiplicity.le_multiplicity_of_le_emultiplicity {α : Type u_1} [Monoid α] {a b : α} (hfin : FiniteMultiplicity 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 FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt {α : Type u_1} [Monoid α] {a b : α} (hfin : FiniteMultiplicity 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 FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity {α : Type u_1} [Monoid α] {a b : α} (hfin : FiniteMultiplicity a b) {n : ℕ} (h : ↑n < emultiplicity a b) : n < multiplicity a b

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

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

theorem FiniteMultiplicity.not_dvd_of_one_right {α : Type u_1} [Monoid α] {a : α} : FiniteMultiplicity 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

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

theorem FiniteMultiplicity.not_isUnit {α : Type u_1} [Monoid α] {a b : α} (h : FiniteMultiplicity a b) : ¬IsUnit a

@[deprecated FiniteMultiplicity.not_isUnit (since := "2026-08-02")]

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

Alias of FiniteMultiplicity.not_isUnit.

theorem FiniteMultiplicity.of_dvd {α : Type u_1} [Monoid α] {a b c : α} (h : b ∣ c) : FiniteMultiplicity a c → FiniteMultiplicity a b

Finiteness of the multiplicity passes to divisors.

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

theorem FiniteMultiplicity.of_pow {α : Type u_1} [Monoid α] {a b : α} {k : ℕ} (hk : k ≠ 0) : FiniteMultiplicity a (b ^ k) → FiniteMultiplicity a b

Finiteness of the multiplicity in a nonzero power passes to the base.

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 FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt {α : Type u_1} [Monoid α] {a b : α} (hf : FiniteMultiplicity 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) (h : FiniteMultiplicity 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 FiniteMultiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [Monoid α] {a b : α} (hf : FiniteMultiplicity 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 FiniteMultiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [Monoid α] {a b : α} (hf : FiniteMultiplicity 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 FiniteMultiplicity.multiplicity_lt_iff_not_dvd {α : Type u_1} [Monoid α] {a b : α} {k : ℕ} (hf : FiniteMultiplicity 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 FiniteMultiplicity.multiplicity_eq_iff {α : Type u_1} [Monoid α] {a b : α} (hf : FiniteMultiplicity a b) {n : ℕ} : multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

theorem emultiplicity_eq_ofNat {a b n : ℕ} [n.AtLeastTwo] : emultiplicity a b = OfNat.ofNat n ↔ a ^ OfNat.ofNat n ∣ b ∧ ¬a ^ (OfNat.ofNat n + 1) ∣ b

@[simp]

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

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

@[simp]

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

@[simp]

theorem multiplicity_one_right {α : Type u_1} [Monoid α] {a : α} : multiplicity a 1 = 0

@[deprecated multiplicity_one_right (since := "2026-09-11")]

theorem FiniteMultiplicity.one_right {α : Type u_1} [Monoid α] {a : α} : multiplicity a 1 = 0

Alias of multiplicity_one_right.

theorem multiplicity_of_isUnit_left {α : Type u_1} [Monoid α] {a : α} (ha : IsUnit a) (b : α) : multiplicity a b = 0

theorem multiplicity_one_left {α : Type u_1} [Monoid α] (b : α) : multiplicity 1 b = 0

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

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

theorem emultiplicity_eq_zero_of_irreducible_ne {R : Type u_3} [CommMonoidWithZero R] [Subsingleton Rˣ] {a b : R} (ha : Irreducible a) (hb : Irreducible b) (h : a ≠ b) : emultiplicity a b = 0

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

theorem multiplicity_eq_zero_of_not_dvd {α : Type u_1} [Monoid α] {a b : α} (h : ¬a ∣ b) : multiplicity a b = 0

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 : α} (h : FiniteMultiplicity a b) : multiplicity a b ≠ 0 ↔ a ∣ b

theorem FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [Monoid α] {a b : α} (hfin : FiniteMultiplicity 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 FiniteMultiplicity.multiplicity_le_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a b : α} {c d : β} (hab : FiniteMultiplicity a b) (hcd : FiniteMultiplicity 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 Associated.finiteMultiplicity_iff_right {α : Type u_1} [Monoid α] {a b c : α} (h : Associated b c) : FiniteMultiplicity a b ↔ FiniteMultiplicity a c

Finiteness of the multiplicity only depends on the associate class of the second argument.

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 : α} (h : FiniteMultiplicity 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.finiteMultiplicity_iff {a b : ℕ} : FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

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

Alias of the reverse direction of dvd_iff_multiplicity_pos.

theorem FiniteMultiplicity.mul_right {α : Type u_1} [CommMonoid α] {a b c : α} (hf : FiniteMultiplicity a (b * c)) : FiniteMultiplicity 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 : α} (hb : IsUnit b) : multiplicity a b = 0

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

@[deprecated multiplicity_one_right (since := "2026-09-11")]

theorem multiplicity_of_one_right {α : Type u_1} [Monoid α] {a : α} : multiplicity a 1 = 0

Alias of multiplicity_one_right.

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 : α} (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 Irreducible.finiteMultiplicity_of_not_isUnit {α : Type u_1} [CommMonoid α] {a x : α} (ha : Irreducible a) (hx : ¬IsUnit x) : FiniteMultiplicity x a

A non-unit has finite multiplicity in an irreducible element.

theorem Irreducible.multiplicity_self {α : Type u_1} [CommMonoid α] {a : α} (ha : Irreducible a) : multiplicity a a = 1

The multiplicity of an irreducible element in itself is 1.

theorem Irreducible.multiplicity_of_associated {α : Type u_1} [CommMonoid α] {a b : α} (ha : Irreducible a) (h : Associated a b) : multiplicity a b = 1

The multiplicity of an irreducible element in an associated element is 1.

theorem Irreducible.multiplicity_eq_ite {α : Type u_1} [CommMonoid α] (p : α) {q : α} [Decidable (Associated p q)] (hq : Irreducible q) : multiplicity p q = if Associated p q then 1 else 0

The multiplicity of p in an irreducible q is 1 if p and q are associated, and 0 otherwise.

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

@[simp]

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

@[deprecated emultiplicity_zero_right (since := "2026-09-11")]

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

Alias of emultiplicity_zero_right.

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

@[deprecated multiplicity_zero_right (since := "2026-09-11")]

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

Alias of multiplicity_zero_right.

@[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_left {α : Type u_1} [MonoidWithZero α] (a : α) : multiplicity 0 a = 0

@[deprecated multiplicity_zero_left (since := "2026-09-11")]

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

Alias of multiplicity_zero_left.

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

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

@[simp]

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

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

Alias of the reverse direction of FiniteMultiplicity.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 FiniteMultiplicity.multiplicity_add_of_gt {α : Type u_1} [Ring α] {p a b : α} (hf : FiniteMultiplicity 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 : FiniteMultiplicity 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) = min (emultiplicity p a) (emultiplicity p b)

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

theorem finiteMultiplicity_mul_aux {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p : α} (hp : Prime p) {a b : α} {n m : ℕ} : ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b

theorem Prime.finiteMultiplicity_mul {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α} (hp : Prime p) : FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b)

theorem FiniteMultiplicity.mul_iff {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α} (hp : Prime p) : FiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b

theorem FiniteMultiplicity.pow {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a : α} (hp : Prime p) (hfin : FiniteMultiplicity p a) {k : ℕ} : FiniteMultiplicity p (a ^ k)

@[simp]

theorem multiplicity_self {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {a : α} (ha : FiniteMultiplicity a a) : multiplicity a a = 1

@[simp]

theorem FiniteMultiplicity.emultiplicity_self {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {a : α} (hfin : FiniteMultiplicity a a) : emultiplicity a a = 1

theorem multiplicity_mul {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) : multiplicity p (a * b) = multiplicity p a + multiplicity p b

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

theorem Finset.emultiplicity_prod {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {β : 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} [CommMonoidWithZero α] [IsCancelMulZero α] {p a : α} (hp : Prime p) {k : ℕ} : emultiplicity p (a ^ k) = ↑k * emultiplicity p a

theorem multiplicity_pow {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a : α} (hp : Prime p) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a

The multiplicity of a prime in a power.

@[deprecated multiplicity_pow (since := "2026-10-29")]

theorem FiniteMultiplicity.multiplicity_pow {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p a : α} (hp : Prime p) : FiniteMultiplicity p a → ∀ {k : ℕ}, multiplicity p (a ^ k) = k * multiplicity p a

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

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

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

theorem multiplicity_pow_self_of_prime {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {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.finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} : FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

theorem Int.finiteMultiplicity_iff {a b : ℤ} : FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

@[instance_reducible]

instance Nat.decidableFiniteMultiplicity : DecidableRel fun (a b : ℕ) => FiniteMultiplicity a b

Equations

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

@[instance_reducible]

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

Equations

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