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.
• FiniteMultiplicity a b: a predicate denoting that the multiplicity of a in b is finite.

@[reducible, inline]

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

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

Equations

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

@[deprecated FiniteMultiplicity (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.

---

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

Equations

• @multiplicity.Finite = @FiniteMultiplicity

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 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 = ⊤ ↔ ¬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 ≠ ⊤

@[deprecated finiteMultiplicity_iff_emultiplicity_ne_top (since := "2024-11-30")]

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

Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

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

Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top.

---

Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

@[deprecated FiniteMultiplicity.emultiplicity_ne_top (since := "2024-11-30")]

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

Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top.

---

Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top.

---

Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

@[deprecated FiniteMultiplicity.emultiplicity_ne_top (since := "2024-11-08")]

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

Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top.

---

Alias of the forward direction of finiteMultiplicity_iff_emultiplicity_ne_top.

---

Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

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

@[deprecated finiteMultiplicity_of_emultiplicity_eq_natCast (since := "2024-11-30")]

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

Alias of finiteMultiplicity_of_emultiplicity_eq_natCast.

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)

@[deprecated FiniteMultiplicity.emultiplicity_eq_multiplicity (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.emultiplicity_eq_multiplicity.

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

@[deprecated FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq.

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_finiteMultiplicity {α : Type u_1} [Monoid α] {a b : α} (h : ¬FiniteMultiplicity a b) : multiplicity a b = 1

@[deprecated multiplicity_eq_one_of_not_finiteMultiplicity (since := "2024-11-30")]

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

Alias of multiplicity_eq_one_of_not_finiteMultiplicity.

@[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 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

@[deprecated FiniteMultiplicity.emultiplicity_le_of_multiplicity_le (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.emultiplicity_le_of_multiplicity_le.

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

@[deprecated FiniteMultiplicity.le_multiplicity_of_le_emultiplicity (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.le_multiplicity_of_le_emultiplicity.

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

@[deprecated FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt.

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

@[deprecated FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity.

theorem emultiplicity_pos_iff {α : Type u_1} [Monoid α] {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

@[deprecated FiniteMultiplicity.def (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.def.

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

@[deprecated FiniteMultiplicity.not_dvd_of_one_right (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_dvd_of_one_right.

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 (since := "2024-04-05")]

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

Alias of Int.natCast_multiplicity.

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

@[deprecated FiniteMultiplicity.not_iff_forall (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_iff_forall.

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

@[deprecated FiniteMultiplicity.not_unit (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_unit.

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

@[deprecated FiniteMultiplicity.mul_left (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.mul_left.

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

@[deprecated FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt.

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 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

@[deprecated FiniteMultiplicity.le_multiplicity_of_pow_dvd (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.le_multiplicity_of_pow_dvd.

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

@[deprecated FiniteMultiplicity.pow_dvd_iff_le_multiplicity (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.pow_dvd_iff_le_multiplicity.

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

@[deprecated FiniteMultiplicity.multiplicity_lt_iff_not_dvd (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.multiplicity_lt_iff_not_dvd.

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

@[deprecated FiniteMultiplicity.multiplicity_eq_iff (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.multiplicity_eq_iff.

@[simp]

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

@[deprecated FiniteMultiplicity.not_of_isUnit_left (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_of_isUnit_left.

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

@[deprecated FiniteMultiplicity.not_of_one_left (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_of_one_left.

@[simp]

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

@[simp]

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

@[deprecated FiniteMultiplicity.one_right (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.one_right.

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

@[deprecated FiniteMultiplicity.not_of_unit_left (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.not_of_unit_left.

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 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

@[deprecated FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd.

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

@[deprecated FiniteMultiplicity.multiplicity_le_multiplicity_iff (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.multiplicity_le_multiplicity_iff.

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

@[deprecated Nat.finiteMultiplicity_iff (since := "2024-11-30")]

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

Alias of Nat.finiteMultiplicity_iff.

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

@[deprecated FiniteMultiplicity.mul_right (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.mul_right.

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 FiniteMultiplicity.ne_zero {α : Type u_1} [MonoidWithZero α] {a b : α} (h : FiniteMultiplicity a b) : b ≠ 0

@[deprecated FiniteMultiplicity.ne_zero (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.ne_zero.

@[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 FiniteMultiplicity.or_of_add {α : Type u_1} [Semiring α] {p a b : α} (hf : FiniteMultiplicity p (a + b)) : FiniteMultiplicity p a ∨ FiniteMultiplicity p b

@[deprecated FiniteMultiplicity.or_of_add (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.or_of_add.

theorem min_le_emultiplicity_add {α : Type u_1} [Semiring α] {p a b : α} : 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

@[deprecated FiniteMultiplicity.neg_iff (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.neg_iff.

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

Alias of the reverse direction of FiniteMultiplicity.neg_iff.

@[deprecated FiniteMultiplicity.neg (since := "2024-11-30")]

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

Alias of the reverse direction of FiniteMultiplicity.neg_iff.

---

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

@[deprecated FiniteMultiplicity.multiplicity_add_of_gt (since := "2024-11-30")]

theorem multiplicity.Finite.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

Alias of FiniteMultiplicity.multiplicity_add_of_gt.

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) = 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) = multiplicity p a ⊓ multiplicity p b

@[irreducible]

theorem finiteMultiplicity_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

@[deprecated finiteMultiplicity_mul_aux (since := "2024-11-30")]

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

Alias of finiteMultiplicity_mul_aux.

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

@[deprecated Prime.finiteMultiplicity_mul (since := "2024-11-30")]

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

Alias of Prime.finiteMultiplicity_mul.

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

@[deprecated FiniteMultiplicity.mul_iff (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.mul_iff.

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

@[deprecated FiniteMultiplicity.pow (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.pow.

@[simp]

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

@[simp]

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

@[deprecated FiniteMultiplicity.emultiplicity_self (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.emultiplicity_self.

theorem multiplicity_mul {α : Type u_1} [CancelCommMonoidWithZero α] {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} [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 FiniteMultiplicity.multiplicity_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p a : α} (hp : Prime p) (ha : FiniteMultiplicity p a) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a

@[deprecated FiniteMultiplicity.multiplicity_pow (since := "2024-11-30")]

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

Alias of FiniteMultiplicity.multiplicity_pow.

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.finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} : FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

@[deprecated Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs (since := "2024-11-30")]

theorem Int.multiplicity_finite_iff_natAbs_finite {a b : ℤ} : FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Alias of Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs.

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

@[deprecated Int.finiteMultiplicity_iff (since := "2024-11-30")]

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

Alias of Int.finiteMultiplicity_iff.

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

Equations

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

@[deprecated Nat.decidableFiniteMultiplicity (since := "2024-11-30")]

def Nat.decidableMultiplicityFinite : DecidableRel fun (a b : ℕ) => FiniteMultiplicity a b

Alias of Nat.decidableFiniteMultiplicity.

Equations

• Nat.decidableMultiplicityFinite = Nat.decidableFiniteMultiplicity

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

Equations

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

@[deprecated Int.decidableMultiplicityFinite (since := "2024-11-30")]

def Int.decidableFiniteMultiplicity : DecidableRel fun (a b : ℤ) => FiniteMultiplicity a b

Alias of Int.decidableMultiplicityFinite.

Equations

• Int.decidableFiniteMultiplicity = Int.decidableMultiplicityFinite