Mathlib.RingTheory.Multiplicity

FiniteMultiplicity abbrev

[Monoid α] (a b : α) : Prop

Full source

/-- `multiplicity.Finite a b` indicates that the multiplicity of `a` in `b` is finite. -/
abbrev FiniteMultiplicity [Monoid α] (a b : α) : Prop :=
  ∃ n : ℕ, ¬a ^ (n + 1) ∣ b

Finite Multiplicity Condition for Monoid Elements

Informal description

For a commutative monoid $\alpha$ and elements $a, b \in \alpha$, the predicate $\text{FiniteMultiplicity}\, a\, b$ holds if there exists a natural number $n$ such that $a^n$ does not divide $b$.

emultiplicity definition

[Monoid α] (a b : α) : ℕ∞

Full source

/-- `emultiplicity a b` returns the largest natural number `n` such that
  `a ^ n ∣ b`, as an `ℕ∞`. If `∀ n, a ^ n ∣ b` then it returns `⊤`. -/
noncomputable def emultiplicity [Monoid α] (a b : α) : ℕ∞ :=
  if h : FiniteMultiplicity a b then Nat.find h else ⊤

Extended multiplicity of a divisor in a commutative monoid

Informal description

For elements $ a $ and $ b $ of a commutative monoid $ \alpha $, the extended multiplicity $ \text{emultiplicity}\, a\, b $ is defined as the largest natural number $ n $ such that $ a^n $ divides $ b $, represented as an element of $ \mathbb{N}_\infty $. If $ a^n $ divides $ b $ for all natural numbers $ n $, then the multiplicity is defined to be $ \infty $. More precisely, $ \text{emultiplicity}\, a\, b $ is defined as follows: - If there exists a natural number $ n $ such that $ a^n $ does not divide $ b $ (i.e., $ \text{FiniteMultiplicity}\, a\, b $ holds), then $ \text{emultiplicity}\, a\, b $ is the largest such $ n $ for which $ a^n $ divides $ b $. - Otherwise, $ \text{emultiplicity}\, a\, b = \infty $.

multiplicity definition

[Monoid α] (a b : α) : ℕ

Full source

/-- A `ℕ`-valued version of `emultiplicity`, returning `1` instead of `⊤`. -/
noncomputable def multiplicity [Monoid α] (a b : α) : ℕ :=
  (emultiplicity a b).untopD 1

Multiplicity of a divisor in a commutative monoid

Informal description

For elements $ a $ and $ b $ of a commutative monoid $ \alpha $, the multiplicity $ \text{multiplicity}\, a\, b $ is defined as the largest natural number $ n $ such that $ a^n $ divides $ b $, with a default value of $ 1 $ when $ a^n $ divides $ b $ for all $ n $ (i.e., when $ \text{emultiplicity}\, a\, b = \infty $).

emultiplicity_eq_top theorem

: emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b

Full source

@[simp]
theorem emultiplicity_eq_top :
    emultiplicityemultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b := by
  simp [emultiplicity]

$\text{emultiplicity}\, a\, b = \infty \leftrightarrow \text{multiplicity is infinite}$

Informal description

For elements $a$ and $b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ equals $\infty$ if and only if the multiplicity of $a$ in $b$ is not finite (i.e., $\neg \text{FiniteMultiplicity}\, a\, b$ holds).

emultiplicity_lt_top theorem

{a b : α} : emultiplicity a b < ⊤ ↔ FiniteMultiplicity a b

Full source

theorem emultiplicity_lt_top {a b : α} : emultiplicityemultiplicity a b < ⊤ ↔ FiniteMultiplicity a b := by
  simp [lt_top_iff_ne_top, emultiplicity_eq_top]

Finite Multiplicity Criterion: $\text{emultiplicity}\, a\, b < \infty \leftrightarrow \text{FiniteMultiplicity}\, a\, b$

Informal description

For elements $a$ and $b$ in a commutative monoid $\alpha$, the extended multiplicity $\text{emultiplicity}\, a\, b$ is strictly less than $\infty$ if and only if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds).

finiteMultiplicity_iff_emultiplicity_ne_top theorem

: FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Full source

theorem finiteMultiplicity_iff_emultiplicity_ne_top :
    FiniteMultiplicityFiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤ := by simp

Finite Multiplicity Criterion: $\text{FiniteMultiplicity}\, a\, b \leftrightarrow \text{emultiplicity}\, a\, b \neq \infty$

Informal description

For elements $a$ and $b$ in a commutative monoid, the multiplicity of $a$ in $b$ is finite if and only if the extended multiplicity $\text{emultiplicity}\, a\, b$ is not equal to $\infty$.

finiteMultiplicity_of_emultiplicity_eq_natCast theorem

{n : ℕ} (h : emultiplicity a b = n) : FiniteMultiplicity a b

Full source

theorem finiteMultiplicity_of_emultiplicity_eq_natCast {n : ℕ} (h : emultiplicity a b = n) :
    FiniteMultiplicity a b := by
  by_contra! nh
  rw [← emultiplicity_eq_top, h] at nh
  trivial

Finite Multiplicity from Extended Multiplicity Equality with Natural Number

Informal description

For any natural number $n$, if the extended multiplicity of $a$ in $b$ equals $n$ (i.e., $\text{emultiplicity}\, a\, b = n$), then the multiplicity of $a$ in $b$ is finite.

multiplicity_eq_of_emultiplicity_eq_some theorem

{n : ℕ} (h : emultiplicity a b = n) : multiplicity a b = n

Full source

theorem multiplicity_eq_of_emultiplicity_eq_some {n : ℕ} (h : emultiplicity a b = n) :
    multiplicity a b = n := by
  simp [multiplicity, h]
  rfl

Multiplicity and Extended Multiplicity Equality: $\text{multiplicity}\, a\, b = n$ when $\text{emultiplicity}\, a\, b = n$

Informal description

For any natural number $n$, if the extended multiplicity of $a$ in $b$ is equal to $n$ (i.e., $\text{emultiplicity}\, a\, b = n$), then the multiplicity of $a$ in $b$ is also equal to $n$ (i.e., $\text{multiplicity}\, a\, b = n$).

emultiplicity_ne_of_multiplicity_ne theorem

{n : ℕ} : multiplicity a b ≠ n → emultiplicity a b ≠ n

Full source

theorem emultiplicity_ne_of_multiplicity_ne {n : ℕ} :
    multiplicitymultiplicity a b ≠ n → emultiplicityemultiplicity a b ≠ n :=
  mt multiplicity_eq_of_emultiplicity_eq_some

Non-equality of Multiplicity Implies Non-equality of Extended Multiplicity: $\text{multiplicity}\, a\, b \neq n \to \text{emultiplicity}\, a\, b \neq n$

Informal description

For any natural number $n$, if the multiplicity of $a$ in $b$ is not equal to $n$ (i.e., $\text{multiplicity}\, a\, b \neq n$), then the extended multiplicity of $a$ in $b$ is also not equal to $n$ (i.e., $\text{emultiplicity}\, a\, b \neq n$).

FiniteMultiplicity.emultiplicity_eq_multiplicity theorem

(h : FiniteMultiplicity a b) : emultiplicity a b = multiplicity a b

Full source

theorem FiniteMultiplicity.emultiplicity_eq_multiplicity (h : FiniteMultiplicity a b) :
    emultiplicity a b = multiplicity a b := by
  cases hm : emultiplicity a b
  · simp [h] at hm
  rw [multiplicity_eq_of_emultiplicity_eq_some hm]

Equality of Extended and Finite Multiplicity

Informal description

For elements $a$ and $b$ of a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds), then the extended multiplicity $\text{emultiplicity}\, a\, b$ equals the multiplicity $\text{multiplicity}\, a\, b$.

FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq theorem

{n : ℕ} (h : FiniteMultiplicity a b) : emultiplicity a b = n ↔ multiplicity a b = n

Full source

theorem FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq {n : ℕ}
    (h : FiniteMultiplicity a b) : emultiplicityemultiplicity a b = n ↔ multiplicity a b = n := by
  simp [h.emultiplicity_eq_multiplicity]

Equivalence of Extended and Finite Multiplicity for Finite Cases

Informal description

For elements $a$ and $b$ of a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds), then for any natural number $n$, the extended multiplicity $\text{emultiplicity}\, a\, b$ equals $n$ if and only if the multiplicity $\text{multiplicity}\, a\, b$ equals $n$. In other words: \[ \text{emultiplicity}\, a\, b = n \leftrightarrow \text{multiplicity}\, a\, b = n. \]

emultiplicity_eq_iff_multiplicity_eq_of_ne_one theorem

{n : ℕ} (h : n ≠ 1) : emultiplicity a b = n ↔ multiplicity a b = n

Full source

theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_one {n : ℕ} (h : n ≠ 1) :
    emultiplicityemultiplicity a b = n ↔ multiplicity a b = n := by
  constructor
  · exact multiplicity_eq_of_emultiplicity_eq_some
  · intro h₂
    simpa [multiplicity, WithTop.untopD_eq_iff, h] using h₂

Equivalence of Extended and Standard Multiplicity for $n \neq 1$

Informal description

For any natural number $n \neq 1$, the extended multiplicity of $a$ in $b$ equals $n$ if and only if the multiplicity of $a$ in $b$ equals $n$. That is, $\text{emultiplicity}\, a\, b = n \leftrightarrow \text{multiplicity}\, a\, b = n$.

emultiplicity_eq_zero_iff_multiplicity_eq_zero theorem

: emultiplicity a b = 0 ↔ multiplicity a b = 0

Full source

theorem emultiplicity_eq_zero_iff_multiplicity_eq_zero :
    emultiplicityemultiplicity a b = 0 ↔ multiplicity a b = 0 :=
  emultiplicity_eq_iff_multiplicity_eq_of_ne_one zero_ne_one

$\text{emultiplicity}\, a\, b = 0 \leftrightarrow \text{multiplicity}\, a\, b = 0$

Informal description

For elements $a$ and $b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ equals $0$ if and only if the multiplicity $\text{multiplicity}\, a\, b$ equals $0$.

multiplicity_eq_one_of_not_finiteMultiplicity theorem

(h : ¬FiniteMultiplicity a b) : multiplicity a b = 1

Full source

@[simp]
theorem multiplicity_eq_one_of_not_finiteMultiplicity (h : ¬FiniteMultiplicity a b) :
    multiplicity a b = 1 := by
  simp [multiplicity, emultiplicity_eq_top.2 h]

Multiplicity equals one when multiplicity is infinite

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is not finite (i.e., $\neg \text{FiniteMultiplicity}\, a\, b$ holds), then $\text{multiplicity}\, a\, b = 1$.

multiplicity_le_emultiplicity theorem

: multiplicity a b ≤ emultiplicity a b

Full source

@[simp]
theorem multiplicity_le_emultiplicity :
    multiplicity a b ≤ emultiplicity a b := by
  by_cases hf : FiniteMultiplicity a b
  · simp [hf.emultiplicity_eq_multiplicity]
  · simp [hf, emultiplicity_eq_top.2]

Multiplicity Bounded by Extended Multiplicity

Informal description

For any elements $a$ and $b$ in a commutative monoid, the multiplicity $\text{multiplicity}\, a\, b$ is less than or equal to the extended multiplicity $\text{emultiplicity}\, a\, b$.

multiplicity_eq_of_emultiplicity_eq theorem

{c d : β} (h : emultiplicity a b = emultiplicity c d) : multiplicity a b = multiplicity c d

Full source

@[simp]
theorem multiplicity_eq_of_emultiplicity_eq {c d : β}
    (h : emultiplicity a b = emultiplicity c d) : multiplicity a b = multiplicity c d := by
  unfold multiplicity
  rw [h]

Multiplicity Equality from Extended Multiplicity Equality

Informal description

For elements $a, b$ in a commutative monoid $\alpha$ and elements $c, d$ in a commutative monoid $\beta$, if the extended multiplicities satisfy $\text{emultiplicity}\, a\, b = \text{emultiplicity}\, c\, d$, then the multiplicities satisfy $\text{multiplicity}\, a\, b = \text{multiplicity}\, c\, d$.

multiplicity_le_of_emultiplicity_le theorem

{n : ℕ} (h : emultiplicity a b ≤ n) : multiplicity a b ≤ n

Full source

theorem multiplicity_le_of_emultiplicity_le {n : ℕ} (h : emultiplicity a b ≤ n) :
    multiplicity a b ≤ n := by
  exact_mod_cast multiplicity_le_emultiplicity.trans h

Multiplicity Bounded by Extended Multiplicity Inequality: $\text{multiplicity}\, a\, b \leq n$ given $\text{emultiplicity}\, a\, b \leq n$

Informal description

For any elements $a$ and $b$ in a commutative monoid and any natural number $n$, if the extended multiplicity $\text{emultiplicity}\, a\, b$ is less than or equal to $n$, then the multiplicity $\text{multiplicity}\, a\, b$ is also less than or equal to $n$.

FiniteMultiplicity.emultiplicity_le_of_multiplicity_le theorem

(hfin : FiniteMultiplicity a b) {n : ℕ} (h : multiplicity a b ≤ n) : emultiplicity a b ≤ n

Full source

theorem FiniteMultiplicity.emultiplicity_le_of_multiplicity_le (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : multiplicity a b ≤ n) : emultiplicity a b ≤ n := by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

Extended Multiplicity Bounded by Finite Multiplicity

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds) and $\text{multiplicity}\, a\, b \leq n$ for some natural number $n$, then $\text{emultiplicity}\, a\, b \leq n$.

le_emultiplicity_of_le_multiplicity theorem

{n : ℕ} (h : n ≤ multiplicity a b) : n ≤ emultiplicity a b

Full source

theorem le_emultiplicity_of_le_multiplicity {n : ℕ} (h : n ≤ multiplicity a b) :
    n ≤ emultiplicity a b := by
  exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

Lower Bound Transfer from Multiplicity to Extended Multiplicity

Informal description

For any natural number $n$ and elements $a$ and $b$ in a commutative monoid, if $n \leq \text{multiplicity}\, a\, b$, then $n \leq \text{emultiplicity}\, a\, b$.

FiniteMultiplicity.le_multiplicity_of_le_emultiplicity theorem

(hfin : FiniteMultiplicity a b) {n : ℕ} (h : n ≤ emultiplicity a b) : n ≤ multiplicity a b

Full source

theorem FiniteMultiplicity.le_multiplicity_of_le_emultiplicity (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : n ≤ emultiplicity a b) : n ≤ multiplicity a b := by
  rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

Lower Bound Transfer from Extended to Finite Multiplicity

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds), then for any natural number $n$, if $n \leq \text{emultiplicity}\, a\, b$, then $n \leq \text{multiplicity}\, a\, b$.

multiplicity_lt_of_emultiplicity_lt theorem

{n : ℕ} (h : emultiplicity a b < n) : multiplicity a b < n

Full source

theorem multiplicity_lt_of_emultiplicity_lt {n : ℕ} (h : emultiplicity a b < n) :
    multiplicity a b < n := by
  exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

Multiplicity Upper Bound from Extended Multiplicity: $\text{emultiplicity}\, a\, b < n \Rightarrow \text{multiplicity}\, a\, b < n$

Informal description

For any natural number $n$ and elements $a$, $b$ in a commutative monoid, if the extended multiplicity $\text{emultiplicity}\, a\, b$ is less than $n$, then the multiplicity $\text{multiplicity}\, a\, b$ is also less than $n$.

FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt theorem

(hfin : FiniteMultiplicity a b) {n : ℕ} (h : multiplicity a b < n) : emultiplicity a b < n

Full source

theorem FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : multiplicity a b < n) : emultiplicity a b < n := by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

Extended multiplicity upper bound from finite multiplicity condition: $\text{multiplicity}\, a\, b < n \Rightarrow \text{emultiplicity}\, a\, b < n$

Informal description

For elements $a$ and $b$ of a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds) and $\text{multiplicity}\, a\, b < n$ for some natural number $n$, then $\text{emultiplicity}\, a\, b < n$.

lt_emultiplicity_of_lt_multiplicity theorem

{n : ℕ} (h : n < multiplicity a b) : n < emultiplicity a b

Full source

theorem lt_emultiplicity_of_lt_multiplicity {n : ℕ} (h : n < multiplicity a b) :
    n < emultiplicity a b := by
  exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

Inequality between Multiplicity and Extended Multiplicity: $n < \text{multiplicity}\, a\, b \Rightarrow n < \text{emultiplicity}\, a\, b$

Informal description

For any natural number $n$ and elements $a$, $b$ in a commutative monoid, if $n$ is less than the multiplicity $\text{multiplicity}\, a\, b$, then $n$ is also less than the extended multiplicity $\text{emultiplicity}\, a\, b$.

FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity theorem

(hfin : FiniteMultiplicity a b) {n : ℕ} (h : n < emultiplicity a b) : n < multiplicity a b

Full source

theorem FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : n < emultiplicity a b) : n < multiplicity a b := by
  rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

Inequality between Extended and Finite Multiplicity: $ n < \text{emultiplicity}\, a\, b $ implies $ n < \text{multiplicity}\, a\, b $ under FiniteMultiplicity

Informal description

For elements $ a $ and $ b $ in a commutative monoid, if the multiplicity of $ a $ in $ b $ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds), then for any natural number $ n $, if $ n < \text{emultiplicity}\, a\, b $, it follows that $ n < \text{multiplicity}\, a\, b $.

emultiplicity_pos_iff theorem

: 0 < emultiplicity a b ↔ 0 < multiplicity a b

Full source

theorem emultiplicity_pos_iff :
    0 < emultiplicity a b ↔ 0 < multiplicity a b := by
  simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

Positivity of Extended Multiplicity and Multiplicity

Informal description

For elements $a$ and $b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ is positive if and only if the multiplicity $\text{multiplicity}\, a\, b$ is positive.

FiniteMultiplicity.def theorem

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

Full source

theorem FiniteMultiplicity.def : FiniteMultiplicityFiniteMultiplicity a b ↔ ∃ n : ℕ, ¬a ^ (n + 1) ∣ b :=
  Iff.rfl

Characterization of Finite Multiplicity via Non-Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the multiplicity of $a$ in $b$ is finite if and only if there exists a natural number $n$ such that $a^{n+1}$ does not divide $b$.

FiniteMultiplicity.not_dvd_of_one_right theorem

: FiniteMultiplicity a 1 → ¬a ∣ 1

Full source

theorem FiniteMultiplicity.not_dvd_of_one_right : FiniteMultiplicity a 1 → ¬a ∣ 1 :=
  fun ⟨n, hn⟩ ⟨d, hd⟩ => hn ⟨d ^ (n + 1), (pow_mul_pow_eq_one (n + 1) hd.symm).symm⟩

Non-divisibility of Identity by Elements with Finite Multiplicity

Informal description

For any element $a$ in a commutative monoid, if the multiplicity of $a$ in the identity element $1$ is finite, then $a$ does not divide $1$.

Int.natCast_emultiplicity theorem

(a b : ℕ) : emultiplicity (a : ℤ) (b : ℤ) = emultiplicity a b

Full source

@[norm_cast]
theorem Int.natCast_emultiplicity (a b : ℕ) :
    emultiplicity (a : ℤ) (b : ℤ) = emultiplicity a b := by
  unfold emultiplicity FiniteMultiplicity
  congr! <;> norm_cast

Preservation of Extended Multiplicity under Integer Casting

Informal description

For any natural numbers $a$ and $b$, the extended multiplicity of $a$ in $b$ as integers is equal to the extended multiplicity of $a$ in $b$ as natural numbers, i.e., \[ \text{emultiplicity}\, (a : \mathbb{Z})\, (b : \mathbb{Z}) = \text{emultiplicity}\, a\, b. \]

Int.natCast_multiplicity theorem

(a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) = multiplicity a b

Full source

@[norm_cast]
theorem Int.natCast_multiplicity (a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) = multiplicity a b :=
  multiplicity_eq_of_emultiplicity_eq (natCast_emultiplicity a b)

Preservation of Multiplicity under Integer Casting

Informal description

For any natural numbers $a$ and $b$, the multiplicity of $a$ in $b$ as integers is equal to the multiplicity of $a$ in $b$ as natural numbers, i.e., \[ \text{multiplicity}\, (a : \mathbb{Z})\, (b : \mathbb{Z}) = \text{multiplicity}\, a\, b. \]

FiniteMultiplicity.not_iff_forall theorem

: ¬FiniteMultiplicity a b ↔ ∀ n : ℕ, a ^ n ∣ b

Full source

theorem FiniteMultiplicity.not_iff_forall : ¬FiniteMultiplicity a b¬FiniteMultiplicity a b ↔ ∀ n : ℕ, a ^ n ∣ b :=
  ⟨fun h n =>
    Nat.casesOn n
      (by
        rw [_root_.pow_zero]
        exact one_dvd _)
      (by simpa [FiniteMultiplicity] using h),
    by simp [FiniteMultiplicity, multiplicity]; tauto⟩

Infinite Multiplicity Characterization via Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the multiplicity of $a$ in $b$ is infinite if and only if $a^n$ divides $b$ for all natural numbers $n$. In other words, $\neg \text{FiniteMultiplicity}\, a\, b \leftrightarrow (\forall n \in \mathbb{N},\, a^n \mid b)$.

FiniteMultiplicity.not_unit theorem

(h : FiniteMultiplicity a b) : ¬IsUnit a

Full source

theorem FiniteMultiplicity.not_unit (h : FiniteMultiplicity a b) : ¬IsUnit a :=
  let ⟨n, hn⟩ := h
  hn ∘ IsUnit.dvd ∘ IsUnit.pow (n + 1)

Non-unit condition for finite multiplicity

Informal description

For any elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite, then $a$ is not a unit.

FiniteMultiplicity.mul_left theorem

{c : α} : FiniteMultiplicity a (b * c) → FiniteMultiplicity a b

Full source

theorem FiniteMultiplicity.mul_left {c : α} :
    FiniteMultiplicity a (b * c) → FiniteMultiplicity a b := fun ⟨n, hn⟩ =>
  ⟨n, fun h => hn (h.trans (dvd_mul_right _ _))⟩

Finite Multiplicity Preserved Under Left Multiplication

Informal description

For elements $a, b, c$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in $b \cdot c$ is finite, then the multiplicity of $a$ in $b$ is also finite.

pow_dvd_of_le_emultiplicity theorem

{k : ℕ} (hk : k ≤ emultiplicity a b) : a ^ k ∣ b

Full source

theorem pow_dvd_of_le_emultiplicity {k : ℕ} (hk : k ≤ emultiplicity a b) :
    a ^ k ∣ b := by classical
  cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Divisibility by Power Bounded by Extended Multiplicity

Informal description

For any natural number $ k $ and elements $ a, b $ in a commutative monoid, if $ k $ is less than or equal to the extended multiplicity of $ a $ in $ b $, then $ a^k $ divides $ b $.

pow_dvd_of_le_multiplicity theorem

{k : ℕ} (hk : k ≤ multiplicity a b) : a ^ k ∣ b

Full source

theorem pow_dvd_of_le_multiplicity {k : ℕ} (hk : k ≤ multiplicity a b) :
    a ^ k ∣ b := pow_dvd_of_le_emultiplicity (le_emultiplicity_of_le_multiplicity hk)

Divisibility by Power Bounded by Multiplicity

Informal description

For any natural number $k$ and elements $a, b$ in a commutative monoid, if $k$ is less than or equal to the multiplicity of $a$ in $b$, then $a^k$ divides $b$.

pow_multiplicity_dvd theorem

(a b : α) : a ^ (multiplicity a b) ∣ b

Full source

@[simp]
theorem pow_multiplicity_dvd (a b : α) : a ^ (multiplicity a b) ∣ b :=
  pow_dvd_of_le_multiplicity le_rfl

Divisibility by Power at Multiplicity Level: $a^{\text{multiplicity}\, a\, b} \mid b$

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the power $a^{\text{multiplicity}\, a\, b}$ divides $b$.

not_pow_dvd_of_emultiplicity_lt theorem

{m : ℕ} (hm : emultiplicity a b < m) : ¬a ^ m ∣ b

Full source

theorem not_pow_dvd_of_emultiplicity_lt {m : ℕ} (hm : emultiplicity a b < m) :
    ¬a ^ m ∣ b := fun nh => by
  unfold emultiplicity at hm
  split at hm
  · simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)
  · simp at hm

Non-divisibility from Extended Multiplicity Bound

Informal description

For any natural number $m$, if the extended multiplicity of $a$ in $b$ is strictly less than $m$, then $a^m$ does not divide $b$.

FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt theorem

(hf : FiniteMultiplicity a b) {m : ℕ} (hm : multiplicity a b < m) : ¬a ^ m ∣ b

Full source

theorem FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt (hf : FiniteMultiplicity a b) {m : ℕ}
    (hm : multiplicity a b < m) : ¬a ^ m ∣ b := by
  apply not_pow_dvd_of_emultiplicity_lt
  rw [hf.emultiplicity_eq_multiplicity]
  norm_cast

Non-divisibility from Finite Multiplicity Bound

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite and the multiplicity value is less than a natural number $m$, then $a^m$ does not divide $b$. In other words, if $\text{FiniteMultiplicity}\, a\, b$ holds and $\text{multiplicity}\, a\, b < m$, then $a^m \nmid b$.

multiplicity_pos_of_dvd theorem

(hdiv : a ∣ b) : 0 < multiplicity a b

Full source

theorem multiplicity_pos_of_dvd (hdiv : a ∣ b) : 0 < multiplicity a b := by
  refine Nat.pos_iff_ne_zero.2 fun h => ?_
  simpa [hdiv] using FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
    (by by_contra! nh; simp [nh] at h) (lt_one_iff.mpr h)

Positivity of multiplicity for divisors

Informal description

For elements $a$ and $b$ in a commutative monoid, if $a$ divides $b$, then the multiplicity of $a$ in $b$ is positive, i.e., $\text{multiplicity}\, a\, b > 0$.

emultiplicity_pos_of_dvd theorem

(hdiv : a ∣ b) : 0 < emultiplicity a b

Full source

theorem emultiplicity_pos_of_dvd (hdiv : a ∣ b) : 0 < emultiplicity a b :=
  lt_emultiplicity_of_lt_multiplicity (multiplicity_pos_of_dvd hdiv)

Positivity of Extended Multiplicity for Divisors

Informal description

For elements $a$ and $b$ in a commutative monoid, if $a$ divides $b$, then the extended multiplicity of $a$ in $b$ is positive, i.e., $\text{emultiplicity}\, a\, b > 0$.

emultiplicity_eq_of_dvd_of_not_dvd theorem

{k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : emultiplicity a b = k

Full source

theorem emultiplicity_eq_of_dvd_of_not_dvd {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) :
    emultiplicity a b = k := by classical
  have : FiniteMultiplicity a b := ⟨k, hsucc⟩
  simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
    Decidable.not_not, true_and]
  exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Extended multiplicity characterization when $a^k \mid b$ but $a^{k+1} \nmid b$

Informal description

For elements $a$ and $b$ in a commutative monoid and a natural number $k$, if $a^k$ divides $b$ but $a^{k+1}$ does not divide $b$, then the extended multiplicity of $a$ in $b$ equals $k$, i.e., $\text{emultiplicity}\, a\, b = k$.

multiplicity_eq_of_dvd_of_not_dvd theorem

{k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) : multiplicity a b = k

Full source

theorem multiplicity_eq_of_dvd_of_not_dvd {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) :
    multiplicity a b = k :=
  multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_of_dvd_of_not_dvd hk hsucc)

Multiplicity Characterization: $\text{multiplicity}\, a\, b = k$ when $a^k \mid b$ but $a^{k+1} \nmid b$

Informal description

For elements $a$ and $b$ in a commutative monoid and a natural number $k$, if $a^k$ divides $b$ but $a^{k+1}$ does not divide $b$, then the multiplicity of $a$ in $b$ equals $k$, i.e., $\text{multiplicity}\, a\, b = k$.

le_emultiplicity_of_pow_dvd theorem

{k : ℕ} (hk : a ^ k ∣ b) : k ≤ emultiplicity a b

Full source

theorem le_emultiplicity_of_pow_dvd {k : ℕ} (hk : a ^ k ∣ b) :
    k ≤ emultiplicity a b :=
  le_of_not_gt fun hk' => not_pow_dvd_of_emultiplicity_lt hk' hk

Lower Bound on Extended Multiplicity from Divisibility

Informal description

For any natural number $k$ and elements $a, b$ in a commutative monoid, if $a^k$ divides $b$, then $k$ is less than or equal to the extended multiplicity of $a$ in $b$, i.e., $k \leq \text{emultiplicity}\, a\, b$.

FiniteMultiplicity.le_multiplicity_of_pow_dvd theorem

(hf : FiniteMultiplicity a b) {k : ℕ} (hk : a ^ k ∣ b) : k ≤ multiplicity a b

Full source

theorem FiniteMultiplicity.le_multiplicity_of_pow_dvd (hf : FiniteMultiplicity a b)
    {k : ℕ} (hk : a ^ k ∣ b) : k ≤ multiplicity a b :=
  hf.le_multiplicity_of_le_emultiplicity (le_emultiplicity_of_pow_dvd hk)

Lower Bound on Multiplicity from Divisibility under Finite Multiplicity Condition

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, a\, b$ holds), then for any natural number $k$, if $a^k$ divides $b$, then $k$ is less than or equal to the multiplicity of $a$ in $b$, i.e., $k \leq \text{multiplicity}\, a\, b$.

pow_dvd_iff_le_emultiplicity theorem

{k : ℕ} : a ^ k ∣ b ↔ k ≤ emultiplicity a b

Full source

theorem pow_dvd_iff_le_emultiplicity {k : ℕ} :
    a ^ k ∣ ba ^ k ∣ b ↔ k ≤ emultiplicity a b :=
  ⟨le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity⟩

Divisibility Condition for Extended Multiplicity: $a^k \mid b \leftrightarrow k \leq \text{emultiplicity}\, a\, b$

Informal description

For any natural number $k$ and elements $a, b$ in a commutative monoid, the power $a^k$ divides $b$ if and only if $k$ is less than or equal to the extended multiplicity of $a$ in $b$, i.e., $a^k \mid b \leftrightarrow k \leq \text{emultiplicity}\, a\, b$.

FiniteMultiplicity.pow_dvd_iff_le_multiplicity theorem

(hf : FiniteMultiplicity a b) {k : ℕ} : a ^ k ∣ b ↔ k ≤ multiplicity a b

Full source

theorem FiniteMultiplicity.pow_dvd_iff_le_multiplicity (hf : FiniteMultiplicity a b) {k : ℕ} :
    a ^ k ∣ ba ^ k ∣ b ↔ k ≤ multiplicity a b := by
  exact_mod_cast hf.emultiplicity_eq_multiplicity ▸ pow_dvd_iff_le_emultiplicity

Divisibility Condition for Finite Multiplicity: $a^k \mid b \leftrightarrow k \leq \text{multiplicity}(a, b)$

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite (i.e., there exists some $n$ such that $a^n \nmid b$), then for any natural number $k$, the power $a^k$ divides $b$ if and only if $k$ is less than or equal to the multiplicity of $a$ in $b$. In other words: $$ a^k \mid b \leftrightarrow k \leq \text{multiplicity}(a, b). $$

emultiplicity_lt_iff_not_dvd theorem

{k : ℕ} : emultiplicity a b < k ↔ ¬a ^ k ∣ b

Full source

theorem emultiplicity_lt_iff_not_dvd {k : ℕ} :
    emultiplicityemultiplicity a b < k ↔ ¬a ^ k ∣ b := by rw [pow_dvd_iff_le_emultiplicity, not_le]

Extended Multiplicity Bound: $\text{emultiplicity}\, a\, b < k \leftrightarrow a^k \nmid b$

Informal description

For any natural number $k$ and elements $a, b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ is less than $k$ if and only if $a^k$ does not divide $b$, i.e., $\text{emultiplicity}\, a\, b < k \leftrightarrow a^k \nmid b$.

FiniteMultiplicity.multiplicity_lt_iff_not_dvd theorem

{k : ℕ} (hf : FiniteMultiplicity a b) : multiplicity a b < k ↔ ¬a ^ k ∣ b

Full source

theorem FiniteMultiplicity.multiplicity_lt_iff_not_dvd {k : ℕ} (hf : FiniteMultiplicity a b) :
    multiplicitymultiplicity a b < k ↔ ¬a ^ k ∣ b := by rw [hf.pow_dvd_iff_le_multiplicity, not_le]

Multiplicity Bound for Finite Multiplicity: $\text{multiplicity}(a, b) < k \leftrightarrow a^k \nmid b$

Informal description

For elements $a$ and $b$ in a commutative monoid, if the multiplicity of $a$ in $b$ is finite, then for any natural number $k$, the multiplicity $\text{multiplicity}(a, b)$ is less than $k$ if and only if $a^k$ does not divide $b$. In other words: $$ \text{multiplicity}(a, b) < k \leftrightarrow a^k \nmid b. $$

emultiplicity_eq_coe theorem

{n : ℕ} : emultiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Full source

theorem emultiplicity_eq_coe {n : ℕ} :
    emultiplicityemultiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b := by
  constructor
  · intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp
  · rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

Characterization of Extended Multiplicity: $\text{emultiplicity}\, a\, b = n \leftrightarrow (a^n \mid b \land a^{n+1} \nmid b)$

Informal description

For elements $a$ and $b$ in a commutative monoid and a natural number $n$, the extended multiplicity $\text{emultiplicity}\, a\, b$ equals $n$ if and only if $a^n$ divides $b$ but $a^{n+1}$ does not divide $b$.

FiniteMultiplicity.multiplicity_eq_iff theorem

(hf : FiniteMultiplicity a b) {n : ℕ} : multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Full source

theorem FiniteMultiplicity.multiplicity_eq_iff (hf : FiniteMultiplicity a b) {n : ℕ} :
    multiplicitymultiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b := by
  simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

Characterization of Finite Multiplicity: $\text{multiplicity}\,a\,b = n \leftrightarrow (a^n \mid b) \land \neg(a^{n+1} \mid b)$

Informal description

Let $a$ and $b$ be elements of a commutative monoid $\alpha$, and suppose the multiplicity of $a$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\,a\,b$ holds). Then for any natural number $n$, the multiplicity $\text{multiplicity}\,a\,b$ equals $n$ if and only if $a^n$ divides $b$ and $a^{n+1}$ does not divide $b$.

emultiplicity_eq_ofNat theorem

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

Full source

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

Characterization of Extended Multiplicity for Numerals $\geq 2$: $\text{emultiplicity}\,a\,b = n \leftrightarrow (a^n \mid b \land a^{n+1} \nmid b)$

Informal description

For natural numbers $a$, $b$, and $n \geq 2$, the extended multiplicity $\text{emultiplicity}\,a\,b$ equals $n$ (as an extended natural number) if and only if $a^n$ divides $b$ and $a^{n+1}$ does not divide $b$.

FiniteMultiplicity.not_of_isUnit_left theorem

(b : α) (ha : IsUnit a) : ¬FiniteMultiplicity a b

Full source

@[simp]
theorem FiniteMultiplicity.not_of_isUnit_left (b : α) (ha : IsUnit a) : ¬FiniteMultiplicity a b :=
  (·.not_unit ha)

Non-finiteness of Multiplicity for Unit Elements

Informal description

For any element $b$ in a commutative monoid $\alpha$ and any unit $a \in \alpha$, the multiplicity of $a$ in $b$ is not finite. That is, $\text{FiniteMultiplicity}\,a\,b$ does not hold when $a$ is a unit.

FiniteMultiplicity.not_of_one_left theorem

(b : α) : ¬FiniteMultiplicity 1 b

Full source

theorem FiniteMultiplicity.not_of_one_left (b : α) : ¬ FiniteMultiplicity 1 b := by simp

Non-finiteness of Multiplicity for the Identity Element

Informal description

For any element $b$ in a commutative monoid $\alpha$, the multiplicity of the identity element $1$ in $b$ is not finite. That is, $\text{FiniteMultiplicity}\,1\,b$ does not hold for any $b \in \alpha$.

emultiplicity_one_left theorem

(b : α) : emultiplicity 1 b = ⊤

Full source

@[simp]
theorem emultiplicity_one_left (b : α) : emultiplicity 1 b = ⊤ :=
  emultiplicity_eq_top.2 (FiniteMultiplicity.not_of_one_left _)

Extended multiplicity of identity is infinite

Informal description

For any element $b$ in a commutative monoid $\alpha$, the extended multiplicity of the identity element $1$ in $b$ is $\infty$, i.e., $\text{emultiplicity}\,1\,b = \infty$.

FiniteMultiplicity.one_right theorem

(ha : FiniteMultiplicity a 1) : multiplicity a 1 = 0

Full source

@[simp]
theorem FiniteMultiplicity.one_right (ha : FiniteMultiplicity a 1) : multiplicity a 1 = 0 := by
  simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

Multiplicity of Divisor in Identity is Zero When Finite

Informal description

For any element $a$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in the identity element $1$ is finite, then $\text{multiplicity}\,a\,1 = 0$.

FiniteMultiplicity.not_of_unit_left theorem

(a : α) (u : αˣ) : ¬FiniteMultiplicity (u : α) a

Full source

theorem FiniteMultiplicity.not_of_unit_left (a : α) (u : αˣ) : ¬ FiniteMultiplicity (u : α) a :=
  FiniteMultiplicity.not_of_isUnit_left a u.isUnit

Non-finiteness of Multiplicity for Unit Elements

Informal description

For any element $a$ in a commutative monoid $\alpha$ and any unit $u \in \alpha$, the multiplicity of $u$ in $a$ is not finite, i.e., $\text{FiniteMultiplicity}\,u\,a$ does not hold.

emultiplicity_eq_zero theorem

: emultiplicity a b = 0 ↔ ¬a ∣ b

Full source

theorem emultiplicity_eq_zero :
    emultiplicityemultiplicity a b = 0 ↔ ¬a ∣ b := by
  by_cases hf : FiniteMultiplicity a b
  · rw [← ENat.coe_zero, emultiplicity_eq_coe]
    simp
  · simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

Zero Extended Multiplicity Characterizes Non-Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ equals zero if and only if $a$ does not divide $b$, i.e., $\text{emultiplicity}\, a\, b = 0 \leftrightarrow a \nmid b$.

multiplicity_eq_zero theorem

: multiplicity a b = 0 ↔ ¬a ∣ b

Full source

theorem multiplicity_eq_zero :
    multiplicitymultiplicity a b = 0 ↔ ¬a ∣ b :=
  (emultiplicity_eq_iff_multiplicity_eq_of_ne_one zero_ne_one).symm.trans emultiplicity_eq_zero

Zero Multiplicity Characterizes Non-Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the multiplicity $\text{multiplicity}(a, b)$ equals zero if and only if $a$ does not divide $b$, i.e., $\text{multiplicity}(a, b) = 0 \leftrightarrow a \nmid b$.

emultiplicity_ne_zero theorem

: emultiplicity a b ≠ 0 ↔ a ∣ b

Full source

theorem emultiplicity_ne_zero :
    emultiplicityemultiplicity a b ≠ 0emultiplicity a b ≠ 0 ↔ a ∣ b := by
  simp [emultiplicity_eq_zero]

Nonzero Extended Multiplicity Characterizes Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the extended multiplicity $\text{emultiplicity}\, a\, b$ is nonzero if and only if $a$ divides $b$, i.e., $\text{emultiplicity}\, a\, b \neq 0 \leftrightarrow a \mid b$.

multiplicity_ne_zero theorem

: multiplicity a b ≠ 0 ↔ a ∣ b

Full source

theorem multiplicity_ne_zero :
    multiplicitymultiplicity a b ≠ 0multiplicity a b ≠ 0 ↔ a ∣ b := by
  simp [multiplicity_eq_zero]

Nonzero Multiplicity Characterizes Divisibility

Informal description

For elements $a$ and $b$ in a commutative monoid, the multiplicity $\text{multiplicity}(a, b)$ is nonzero if and only if $a$ divides $b$, i.e., $\text{multiplicity}(a, b) \neq 0 \leftrightarrow a \mid b$.

FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd theorem

(hfin : FiniteMultiplicity a b) : ∃ c : α, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Full source

theorem FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd (hfin : FiniteMultiplicity a b) :
    ∃ c : α, b = a ^ multiplicity a b * c ∧ ¬a ∣ c := by
  obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b
  refine ⟨c, hc, ?_⟩
  rintro ⟨k, hk⟩
  rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc
  have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩
  exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

Factorization at Multiplicity Level: $b = a^n \cdot c$ with $a \nmid c$

Informal description

For elements $a$ and $b$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in $b$ is finite, then there exists an element $c \in \alpha$ such that $b = a^{\text{multiplicity}\, a\, b} \cdot c$ and $a$ does not divide $c$.

emultiplicity_le_emultiplicity_iff theorem

{c d : β} : emultiplicity a b ≤ emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d

Full source

theorem emultiplicity_le_emultiplicity_iff {c d : β} :
    emultiplicityemultiplicity a b ≤ emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d := by classical
  constructor
  · exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
  · intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.coe_ne_top, imp_false, not_false_eq_true, implies_true]

Comparison of Extended Multiplicities via Divisibility Conditions

Informal description

For elements $a, b, c, d$ in a commutative monoid $\beta$, the extended multiplicity of $a$ in $b$ is less than or equal to the extended multiplicity of $c$ in $d$ if and only if for every natural number $n$, if $a^n$ divides $b$ then $c^n$ divides $d$. In other words, $\text{emultiplicity}\, a\, b \leq \text{emultiplicity}\, c\, d \leftrightarrow (\forall n \in \mathbb{N}, a^n \mid b \rightarrow c^n \mid d)$.

FiniteMultiplicity.multiplicity_le_multiplicity_iff theorem

 {c d : β} (hab : FiniteMultiplicity a b) (hcd : FiniteMultiplicity c d) :
  multiplicity a b ≤ multiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d

Full source

theorem FiniteMultiplicity.multiplicity_le_multiplicity_iff {c d : β} (hab : FiniteMultiplicity a b)
    (hcd : FiniteMultiplicity c d) :
    multiplicitymultiplicity a b ≤ multiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d := by
  rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hab.emultiplicity_eq_multiplicity,
    ← hcd.emultiplicity_eq_multiplicity]
  apply emultiplicity_le_emultiplicity_iff

Comparison of Finite Multiplicities via Divisibility Conditions

Informal description

For elements $a, b, c, d$ in a commutative monoid $\beta$, if the multiplicities of $a$ in $b$ and $c$ in $d$ are both finite, then the multiplicity of $a$ in $b$ is less than or equal to the multiplicity of $c$ in $d$ if and only if for every natural number $n$, if $a^n$ divides $b$ then $c^n$ divides $d$. In other words, under the conditions $\text{FiniteMultiplicity}\, a\, b$ and $\text{FiniteMultiplicity}\, c\, d$, we have: $$\text{multiplicity}\, a\, b \leq \text{multiplicity}\, c\, d \leftrightarrow (\forall n \in \mathbb{N}, a^n \mid b \rightarrow c^n \mid d)$$

emultiplicity_eq_emultiplicity_iff theorem

{c d : β} : emultiplicity a b = emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b ↔ c ^ n ∣ d

Full source

theorem emultiplicity_eq_emultiplicity_iff {c d : β} :
    emultiplicityemultiplicity a b = emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b ↔ c ^ n ∣ d :=
  ⟨fun h n =>
    ⟨emultiplicity_le_emultiplicity_iff.1 h.le n, emultiplicity_le_emultiplicity_iff.1 h.ge n⟩,
    fun h => le_antisymm (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mp)
      (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mpr)⟩

Equality of Extended Multiplicities via Divisibility Equivalence

Informal description

For elements $a, b, c, d$ in a commutative monoid $\beta$, the extended multiplicity of $a$ in $b$ is equal to the extended multiplicity of $c$ in $d$ if and only if for every natural number $n$, $a^n$ divides $b$ precisely when $c^n$ divides $d$. In other words, $\text{emultiplicity}\, a\, b = \text{emultiplicity}\, c\, d \leftrightarrow (\forall n \in \mathbb{N}, a^n \mid b \leftrightarrow c^n \mid d)$.

le_emultiplicity_map theorem

 {F : Type*} [FunLike F α β] [MonoidHomClass F α β] (f : F) {a b : α} : emultiplicity a b ≤ emultiplicity (f a) (f b)

Full source

theorem le_emultiplicity_map {F : Type*} [FunLike F α β] [MonoidHomClass F α β]
    (f : F) {a b : α} :
    emultiplicity a b ≤ emultiplicity (f a) (f b) :=
  emultiplicity_le_emultiplicity_iff.2 fun n ↦ by rw [← map_pow]; exact map_dvd f

Monotonicity of Extended Multiplicity under Monoid Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve the monoid structure. For any homomorphism $f \in F$ and elements $a, b \in \alpha$, the extended multiplicity of $a$ in $b$ is less than or equal to the extended multiplicity of $f(a)$ in $f(b)$, i.e., \[ \text{emultiplicity}\, a\, b \leq \text{emultiplicity}\, (f\, a)\, (f\, b). \]

emultiplicity_map_eq theorem

 {F : Type*} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a b : α} : emultiplicity (f a) (f b) = emultiplicity a b

Full source

theorem emultiplicity_map_eq {F : Type*} [EquivLike F α β] [MulEquivClass F α β]
    (f : F) {a b : α} : emultiplicity (f a) (f b) = emultiplicity a b := by
  simp [emultiplicity_eq_emultiplicity_iff, ← map_pow, map_dvd_iff]

Invariance of Extended Multiplicity under Multiplicative Equivalence

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type equipped with an equivalence-like structure between $\alpha$ and $\beta$ that preserves the multiplicative structure (i.e., $[EquivLike\, F\, \alpha\, \beta]$ and $[MulEquivClass\, F\, \alpha\, \beta]$). For any $f \in F$ and elements $a, b \in \alpha$, the extended multiplicity of $f(a)$ in $f(b)$ equals the extended multiplicity of $a$ in $b$, i.e., \[ \text{emultiplicity}\, (f\, a)\, (f\, b) = \text{emultiplicity}\, a\, b. \]

multiplicity_map_eq theorem

 {F : Type*} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a b : α} : multiplicity (f a) (f b) = multiplicity a b

Full source

theorem multiplicity_map_eq {F : Type*} [EquivLike F α β] [MulEquivClass F α β]
    (f : F) {a b : α} : multiplicity (f a) (f b) = multiplicity a b :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_map_eq f)

Invariance of Multiplicity under Multiplicative Equivalence

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type equipped with an equivalence-like structure between $\alpha$ and $\beta$ that preserves the multiplicative structure. For any $f \in F$ and elements $a, b \in \alpha$, the multiplicity of $f(a)$ in $f(b)$ equals the multiplicity of $a$ in $b$, i.e., \[ \text{multiplicity}\, (f\, a)\, (f\, b) = \text{multiplicity}\, a\, b. \]

emultiplicity_le_emultiplicity_of_dvd_right theorem

{a b c : α} (h : b ∣ c) : emultiplicity a b ≤ emultiplicity a c

Full source

theorem emultiplicity_le_emultiplicity_of_dvd_right {a b c : α} (h : b ∣ c) :
    emultiplicity a b ≤ emultiplicity a c :=
  emultiplicity_le_emultiplicity_iff.2 fun _ hb => hb.trans h

Extended Multiplicity Increases with Divisibility on the Right

Informal description

For elements $a, b, c$ in a commutative monoid $\alpha$, if $b$ divides $c$ (i.e., $b \mid c$), then the extended multiplicity of $a$ in $b$ is less than or equal to the extended multiplicity of $a$ in $c$, i.e., \[ \text{emultiplicity}\, a\, b \leq \text{emultiplicity}\, a\, c. \]

emultiplicity_eq_of_associated_right theorem

{a b c : α} (h : Associated b c) : emultiplicity a b = emultiplicity a c

Full source

theorem emultiplicity_eq_of_associated_right {a b c : α} (h : Associated b c) :
    emultiplicity a b = emultiplicity a c :=
  le_antisymm (emultiplicity_le_emultiplicity_of_dvd_right h.dvd)
    (emultiplicity_le_emultiplicity_of_dvd_right h.symm.dvd)

Invariance of Extended Multiplicity under Associated Elements

Informal description

For any elements $a, b, c$ in a commutative monoid $\alpha$, if $b$ and $c$ are associated (i.e., $b$ and $c$ differ by a unit), then the extended multiplicity of $a$ in $b$ equals the extended multiplicity of $a$ in $c$, i.e., \[ \text{emultiplicity}\, a\, b = \text{emultiplicity}\, a\, c. \]

multiplicity_eq_of_associated_right theorem

{a b c : α} (h : Associated b c) : multiplicity a b = multiplicity a c

Full source

theorem multiplicity_eq_of_associated_right {a b c : α} (h : Associated b c) :
    multiplicity a b = multiplicity a c :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_right h)

Invariance of Multiplicity under Associated Elements

Informal description

For any elements $a, b, c$ in a commutative monoid $\alpha$, if $b$ and $c$ are associated (i.e., $b$ and $c$ differ by a unit), then the multiplicity of $a$ in $b$ equals the multiplicity of $a$ in $c$, i.e., \[ \text{multiplicity}\, a\, b = \text{multiplicity}\, a\, c. \]

dvd_of_emultiplicity_pos theorem

{a b : α} (h : 0 < emultiplicity a b) : a ∣ b

Full source

theorem dvd_of_emultiplicity_pos {a b : α} (h : 0 < emultiplicity a b) : a ∣ b :=
  pow_one a ▸ pow_dvd_of_le_emultiplicity (Order.add_one_le_of_lt h)

Divisibility from Positive Extended Multiplicity

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, if the extended multiplicity $\text{emultiplicity}\,a\,b$ is positive (i.e., $0 < \text{emultiplicity}\,a\,b$), then $a$ divides $b$ (i.e., $a \mid b$).

dvd_of_multiplicity_pos theorem

{a b : α} (h : 0 < multiplicity a b) : a ∣ b

Full source

theorem dvd_of_multiplicity_pos {a b : α} (h : 0 < multiplicity a b) : a ∣ b :=
  dvd_of_emultiplicity_pos (lt_emultiplicity_of_lt_multiplicity h)

Divisibility from Positive Multiplicity

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, if the multiplicity $\text{multiplicity}\,a\,b$ is positive (i.e., $0 < \text{multiplicity}\,a\,b$), then $a$ divides $b$ (i.e., $a \mid b$).

dvd_iff_multiplicity_pos theorem

{a b : α} : 0 < multiplicity a b ↔ a ∣ b

Full source

theorem dvd_iff_multiplicity_pos {a b : α} : 0 < multiplicity a b ↔ a ∣ b :=
  ⟨dvd_of_multiplicity_pos, fun hdvd => Nat.pos_of_ne_zero (by simpa [multiplicity_eq_zero])⟩

Positive Multiplicity Characterizes Divisibility: $0 < \text{multiplicity}(a, b) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the multiplicity of $a$ in $b$ is positive (i.e., $0 < \text{multiplicity}(a, b)$) if and only if $a$ divides $b$ (i.e., $a \mid b$).

dvd_iff_emultiplicity_pos theorem

{a b : α} : 0 < emultiplicity a b ↔ a ∣ b

Full source

theorem dvd_iff_emultiplicity_pos {a b : α} : 0 < emultiplicity a b ↔ a ∣ b :=
  emultiplicity_pos_iff.trans dvd_iff_multiplicity_pos

Positive Extended Multiplicity Characterizes Divisibility: $0 < \text{emultiplicity}(a, b) \leftrightarrow a \mid b$

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the extended multiplicity $\text{emultiplicity}(a, b)$ is positive (i.e., $0 < \text{emultiplicity}(a, b)$) if and only if $a$ divides $b$ (i.e., $a \mid b$).

Nat.finiteMultiplicity_iff theorem

{a b : ℕ} : FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Full source

theorem Nat.finiteMultiplicity_iff {a b : ℕ} : FiniteMultiplicityFiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b := by
  rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt,
    Nat.le_zero]
  exact
    ⟨fun h =>
      or_iff_not_imp_right.2 fun hb =>
        have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
        Classical.by_contradiction fun ha1 : a ≠ 1 =>
          have ha_gt_one : 1 < a :=
            lt_of_not_ge fun _ =>
              match a with
              | 0 => ha rfl
              | 1 => ha1 rfl
              | b+2 => by omega
          not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
      fun h => by cases h <;> simp [*]⟩

Finite Multiplicity Criterion for Natural Numbers: $a \neq 1$ and $b > 0$

Informal description

For natural numbers $a$ and $b$, the multiplicity of $a$ in $b$ is finite if and only if $a \neq 1$ and $b > 0$.

FiniteMultiplicity.mul_right theorem

{a b c : α} (hf : FiniteMultiplicity a (b * c)) : FiniteMultiplicity a c

Full source

theorem FiniteMultiplicity.mul_right {a b c : α} (hf : FiniteMultiplicity a (b * c)) :
    FiniteMultiplicity a c := (mul_comm b c ▸ hf).mul_left

Finite Multiplicity Preserved Under Right Multiplication

Informal description

For elements $a, b, c$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in the product $b \cdot c$ is finite, then the multiplicity of $a$ in $c$ is also finite.

emultiplicity_of_isUnit_right theorem

{a b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : emultiplicity a b = 0

Full source

theorem emultiplicity_of_isUnit_right {a b : α} (ha : ¬IsUnit a)
    (hb : IsUnit b) : emultiplicity a b = 0 :=
  emultiplicity_eq_zero.mpr fun h ↦ ha (isUnit_of_dvd_unit h hb)

Extended Multiplicity Vanishes for Non-Unit Divisor and Unit Dividend

Informal description

For elements $a$ and $b$ in a commutative monoid $\alpha$, if $a$ is not a unit and $b$ is a unit, then the extended multiplicity $\text{emultiplicity}\, a\, b$ is zero.

multiplicity_of_isUnit_right theorem

{a b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : multiplicity a b = 0

Full source

theorem multiplicity_of_isUnit_right {a b : α} (ha : ¬IsUnit a)
    (hb : IsUnit b) : multiplicity a b = 0 :=
  multiplicity_eq_zero.mpr fun h ↦ ha (isUnit_of_dvd_unit h hb)

Multiplicity Vanishes for Non-Unit Divisor and Unit Dividend

Informal description

For elements $a$ and $b$ in a commutative monoid $\alpha$, if $a$ is not a unit and $b$ is a unit, then the multiplicity $\text{multiplicity}(a, b)$ is zero.

emultiplicity_of_one_right theorem

{a : α} (ha : ¬IsUnit a) : emultiplicity a 1 = 0

Full source

theorem emultiplicity_of_one_right {a : α} (ha : ¬IsUnit a) : emultiplicity a 1 = 0 :=
  emultiplicity_of_isUnit_right ha isUnit_one

Extended multiplicity of non-unit divisor for identity is zero

Informal description

For any element $a$ in a commutative monoid $\alpha$ that is not a unit, the extended multiplicity of $a$ dividing the multiplicative identity $1$ is zero, i.e., $\text{emultiplicity}\, a\, 1 = 0$.

multiplicity_of_one_right theorem

{a : α} (ha : ¬IsUnit a) : multiplicity a 1 = 0

Full source

theorem multiplicity_of_one_right {a : α} (ha : ¬IsUnit a) : multiplicity a 1 = 0 :=
  multiplicity_of_isUnit_right ha isUnit_one

Multiplicity of Non-Unit Divisor for Identity is Zero

Informal description

For any element $a$ in a commutative monoid $\alpha$ that is not a unit, the multiplicity of $a$ dividing the multiplicative identity $1$ is zero, i.e., $\text{multiplicity}(a, 1) = 0$.

emultiplicity_of_unit_right theorem

{a : α} (ha : ¬IsUnit a) (u : αˣ) : emultiplicity a u = 0

Full source

theorem emultiplicity_of_unit_right {a : α} (ha : ¬IsUnit a) (u : αˣ) : emultiplicity a u = 0 :=
  emultiplicity_of_isUnit_right ha u.isUnit

Extended Multiplicity Vanishes for Non-Unit Divisor and Unit Element

Informal description

For any element $a$ in a commutative monoid $\alpha$ that is not a unit, and for any unit $u$ in $\alpha$, the extended multiplicity of $a$ in $u$ is zero, i.e., $\text{emultiplicity}\, a\, u = 0$.

multiplicity_of_unit_right theorem

{a : α} (ha : ¬IsUnit a) (u : αˣ) : multiplicity a u = 0

Full source

theorem multiplicity_of_unit_right {a : α} (ha : ¬IsUnit a) (u : αˣ) : multiplicity a u = 0 :=
  multiplicity_of_isUnit_right ha u.isUnit

Multiplicity of Non-Unit in Unit is Zero

Informal description

For any non-unit element $a$ in a commutative monoid $\alpha$ and any unit $u$ in $\alpha$, the multiplicity of $a$ in $u$ is zero, i.e., $\text{multiplicity}(a, u) = 0$.

emultiplicity_le_emultiplicity_of_dvd_left theorem

{a b c : α} (hdvd : a ∣ b) : emultiplicity b c ≤ emultiplicity a c

Full source

theorem emultiplicity_le_emultiplicity_of_dvd_left {a b c : α} (hdvd : a ∣ b) :
    emultiplicity b c ≤ emultiplicity a c :=
  emultiplicity_le_emultiplicity_iff.2 fun n h => (pow_dvd_pow_of_dvd hdvd n).trans h

Extended Multiplicity Decreases When Divisor Increases

Informal description

For any elements $a, b, c$ in a commutative monoid $\alpha$, if $a$ divides $b$ (i.e., $a \mid b$), then the extended multiplicity of $b$ in $c$ is less than or equal to the extended multiplicity of $a$ in $c$. In other words, $a \mid b$ implies $\text{emultiplicity}\, b\, c \leq \text{emultiplicity}\, a\, c$.

emultiplicity_eq_of_associated_left theorem

{a b c : α} (h : Associated a b) : emultiplicity b c = emultiplicity a c

Full source

theorem emultiplicity_eq_of_associated_left {a b c : α} (h : Associated a b) :
    emultiplicity b c = emultiplicity a c :=
  le_antisymm (emultiplicity_le_emultiplicity_of_dvd_left h.dvd)
    (emultiplicity_le_emultiplicity_of_dvd_left h.symm.dvd)

Extended Multiplicity is Invariant Under Associated Elements

Informal description

For any elements $a, b, c$ in a commutative monoid $\alpha$, if $a$ and $b$ are associated (i.e., $a$ and $b$ differ by a unit), then the extended multiplicity of $b$ in $c$ is equal to the extended multiplicity of $a$ in $c$. In other words, $a \sim b$ implies $\text{emultiplicity}\, b\, c = \text{emultiplicity}\, a\, c$.

multiplicity_eq_of_associated_left theorem

{a b c : α} (h : Associated a b) : multiplicity b c = multiplicity a c

Full source

theorem multiplicity_eq_of_associated_left {a b c : α} (h : Associated a b) :
    multiplicity b c = multiplicity a c :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_eq_of_associated_left h)

Multiplicity Invariance Under Associated Elements

Informal description

For any elements $a$, $b$, and $c$ in a commutative monoid $\alpha$, if $a$ and $b$ are associated (i.e., $a = ub$ for some unit $u$), then the multiplicity of $b$ in $c$ equals the multiplicity of $a$ in $c$. In other words, $a \sim b$ implies $\text{multiplicity}(b, c) = \text{multiplicity}(a, c)$.

emultiplicity_mk_eq_emultiplicity theorem

{a b : α} : emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

Full source

theorem emultiplicity_mk_eq_emultiplicity {a b : α} :
    emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b := by
  simp [emultiplicity_eq_emultiplicity_iff, ← Associates.mk_pow, Associates.mk_dvd_mk]

Equality of Extended Multiplicity for Associate Classes

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the extended multiplicity of the associate class of $a$ in the associate class of $b$ is equal to the extended multiplicity of $a$ in $b$. That is, \[ \text{emultiplicity}\, (\text{Associates.mk}\, a)\, (\text{Associates.mk}\, b) = \text{emultiplicity}\, a\, b. \]

FiniteMultiplicity.ne_zero theorem

{a b : α} (h : FiniteMultiplicity a b) : b ≠ 0

Full source

theorem FiniteMultiplicity.ne_zero {a b : α} (h : FiniteMultiplicity a b) : b ≠ 0 :=
  let ⟨n, hn⟩ := h
  fun hb => by simp [hb] at hn

Nonzero Condition for Finite Multiplicity

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in $b$ is finite, then $b$ is not equal to the zero element of $\alpha$.

emultiplicity_zero theorem

(a : α) : emultiplicity a 0 = ⊤

Full source

@[simp]
theorem emultiplicity_zero (a : α) : emultiplicity a 0 = ⊤ :=
  emultiplicity_eq_top.2 (fun v ↦ v.ne_zero rfl)

Extended multiplicity of any element in zero is infinite

Informal description

For any element $a$ in a commutative monoid $\alpha$, the extended multiplicity of $a$ in the zero element is infinity, i.e., $\text{emultiplicity}\, a\, 0 = \infty$.

emultiplicity_zero_eq_zero_of_ne_zero theorem

(a : α) (ha : a ≠ 0) : emultiplicity 0 a = 0

Full source

@[simp]
theorem emultiplicity_zero_eq_zero_of_ne_zero (a : α) (ha : a ≠ 0) : emultiplicity 0 a = 0 :=
  emultiplicity_eq_zero.2 <| mt zero_dvd_iff.1 ha

Zero Multiplicity of Zero in Nonzero Elements: $\text{emultiplicity}\, 0\, a = 0$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a commutative monoid $\alpha$, the extended multiplicity of the zero element in $a$ is zero, i.e., $\text{emultiplicity}\, 0\, a = 0$.

multiplicity_zero_eq_zero_of_ne_zero theorem

(a : α) (ha : a ≠ 0) : multiplicity 0 a = 0

Full source

@[simp]
theorem multiplicity_zero_eq_zero_of_ne_zero (a : α) (ha : a ≠ 0) : multiplicity 0 a = 0 :=
  multiplicity_eq_zero.2 <| mt zero_dvd_iff.1 ha

Multiplicity of Zero in Nonzero Elements is Zero: $\text{multiplicity}(0, a) = 0$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a commutative monoid $\alpha$, the multiplicity of the zero element in $a$ is zero, i.e., $\text{multiplicity}(0, a) = 0$.

FiniteMultiplicity.or_of_add theorem

{p a b : α} (hf : FiniteMultiplicity p (a + b)) : FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Full source

theorem FiniteMultiplicity.or_of_add {p a b : α} (hf : FiniteMultiplicity p (a + b)) :
    FiniteMultiplicityFiniteMultiplicity p a ∨ FiniteMultiplicity p b := by
  by_contra! nh
  obtain ⟨c, hc⟩ := hf
  simp_all [dvd_add]

Finite Multiplicity is Preserved Under Addition in Commutative Monoids

Informal description

For elements $p, a, b$ in a commutative monoid $\alpha$, if the multiplicity of $p$ in $a + b$ is finite, then the multiplicity of $p$ in $a$ or the multiplicity of $p$ in $b$ is finite. In other words, if $\text{FiniteMultiplicity}\, p\, (a + b)$ holds, then $\text{FiniteMultiplicity}\, p\, a$ or $\text{FiniteMultiplicity}\, p\, b$ holds.

min_le_emultiplicity_add theorem

{p a b : α} : min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Full source

theorem min_le_emultiplicity_add {p a b : α} :
    min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b) := by
  cases hm : min (emultiplicity p a) (emultiplicity p b)
  · simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
    contrapose hm
    simp only [not_and_or, not_not] at hm ⊢
    exact hm.or_of_add
  · apply le_emultiplicity_of_pow_dvd
    simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

Minimum Extended Multiplicity Bound for Sums in Commutative Monoids

Informal description

For any elements $p, a, b$ in a commutative monoid $\alpha$, the minimum of the extended multiplicities of $p$ in $a$ and $p$ in $b$ is less than or equal to the extended multiplicity of $p$ in $a + b$. That is, \[ \min(\text{emultiplicity}\, p\, a, \text{emultiplicity}\, p\, b) \leq \text{emultiplicity}\, p\, (a + b). \]

FiniteMultiplicity.neg_iff theorem

{a b : α} : FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Full source

@[simp]
theorem FiniteMultiplicity.neg_iff {a b : α} :
    FiniteMultiplicityFiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b := by
  unfold FiniteMultiplicity
  congr! 3
  simp only [dvd_neg]

Finite Multiplicity Preservation under Negation

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the multiplicity of $a$ in $-b$ is finite if and only if the multiplicity of $a$ in $b$ is finite. That is, $\text{FiniteMultiplicity}\, a\, (-b) \leftrightarrow \text{FiniteMultiplicity}\, a\, b$.

emultiplicity_neg theorem

(a b : α) : emultiplicity a (-b) = emultiplicity a b

Full source

@[simp]
theorem emultiplicity_neg (a b : α) : emultiplicity a (-b) = emultiplicity a b := by
  rw [emultiplicity_eq_emultiplicity_iff]
  simp

Extended Multiplicity is Invariant under Negation: $\text{emultiplicity}\, a\, (-b) = \text{emultiplicity}\, a\, b$

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the extended multiplicity of $a$ in $-b$ is equal to the extended multiplicity of $a$ in $b$, i.e., \[ \text{emultiplicity}\, a\, (-b) = \text{emultiplicity}\, a\, b. \]

multiplicity_neg theorem

(a b : α) : multiplicity a (-b) = multiplicity a b

Full source

@[simp]
theorem multiplicity_neg (a b : α) : multiplicity a (-b) = multiplicity a b :=
  multiplicity_eq_of_emultiplicity_eq (emultiplicity_neg a b)

Multiplicity is Invariant under Negation: $\text{multiplicity}\, a\, (-b) = \text{multiplicity}\, a\, b$

Informal description

For any elements $a$ and $b$ in a commutative monoid $\alpha$, the multiplicity of $a$ in $-b$ is equal to the multiplicity of $a$ in $b$, i.e., \[ \text{multiplicity}\, a\, (-b) = \text{multiplicity}\, a\, b. \]

Int.emultiplicity_natAbs theorem

(a : ℕ) (b : ℤ) : emultiplicity a b.natAbs = emultiplicity (a : ℤ) b

Full source

theorem Int.emultiplicity_natAbs (a : ℕ) (b : ℤ) :
    emultiplicity a b.natAbs = emultiplicity (a : ℤ) b := by
  rcases Int.natAbs_eq b with h | h <;> conv_rhs => rw [h]
  · rw [Int.natCast_emultiplicity]
  · rw [emultiplicity_neg, Int.natCast_emultiplicity]

Extended Multiplicity of Natural Number in Absolute Value Equals Extended Multiplicity in Integer

Informal description

For any natural number $a$ and integer $b$, the extended multiplicity of $a$ in the natural number $|b|$ (the absolute value of $b$) is equal to the extended multiplicity of the integer $a$ in $b$, i.e., \[ \text{emultiplicity}\, a\, |b| = \text{emultiplicity}\, (a : \mathbb{Z})\, b. \]

Int.multiplicity_natAbs theorem

(a : ℕ) (b : ℤ) : multiplicity a b.natAbs = multiplicity (a : ℤ) b

Full source

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

Multiplicity of Natural Number in Absolute Value Equals Multiplicity in Integer

Informal description

For any natural number $a$ and integer $b$, the multiplicity of $a$ in the natural number $|b|$ (the absolute value of $b$) is equal to the multiplicity of the integer $a$ in $b$, i.e., \[ \text{multiplicity}\, a\, |b| = \text{multiplicity}\, (a : \mathbb{Z})\, b. \]

emultiplicity_add_of_gt theorem

{p a b : α} (h : emultiplicity p b < emultiplicity p a) : emultiplicity p (a + b) = emultiplicity p b

Full source

theorem emultiplicity_add_of_gt {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
    emultiplicity p (a + b) = emultiplicity p b := by
  have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
  rw [this.emultiplicity_eq_multiplicity] at *
  apply emultiplicity_eq_of_dvd_of_not_dvd
  · apply dvd_add
    · apply pow_dvd_of_le_emultiplicity
      exact h.le
    · simp
  · rw [dvd_add_right]
    · apply this.not_pow_dvd_of_multiplicity_lt
      simp
    apply pow_dvd_of_le_emultiplicity
    exact Order.add_one_le_of_lt h

Extended Multiplicity of Sum When Multiplicities Are Ordered: $\text{emultiplicity}\, p\, (a + b) = \text{emultiplicity}\, p\, b$ if $\text{emultiplicity}\, p\, b < \text{emultiplicity}\, p\, a$

Informal description

For elements $p$, $a$, and $b$ in a commutative monoid $\alpha$, if the extended multiplicity of $p$ in $b$ is strictly less than the extended multiplicity of $p$ in $a$, then the extended multiplicity of $p$ in the sum $a + b$ equals the extended multiplicity of $p$ in $b$, i.e., $\text{emultiplicity}\, p\, (a + b) = \text{emultiplicity}\, p\, b$.

FiniteMultiplicity.multiplicity_add_of_gt theorem

 {p a b : α} (hf : FiniteMultiplicity p b) (h : multiplicity p b < multiplicity p a) :
  multiplicity p (a + b) = multiplicity p b

Full source

theorem FiniteMultiplicity.multiplicity_add_of_gt {p a b : α} (hf : FiniteMultiplicity p b)
    (h : multiplicity p b < multiplicity p a) :
    multiplicity p (a + b) = multiplicity p b :=
  multiplicity_eq_of_emultiplicity_eq <| emultiplicity_add_of_gt (hf.emultiplicity_eq_multiplicity ▸
      (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity)

Multiplicity of Sum When Multiplicities Are Ordered and Finite: $\text{multiplicity}\, p\, (a + b) = \text{multiplicity}\, p\, b$ if $\text{multiplicity}\, p\, b < \text{multiplicity}\, p\, a$ and finite

Informal description

Let $p$, $a$, and $b$ be elements of a commutative monoid $\alpha$. If the multiplicity of $p$ in $b$ is finite (i.e., $\text{FiniteMultiplicity}\, p\, b$ holds) and the multiplicity of $p$ in $b$ is strictly less than the multiplicity of $p$ in $a$, then the multiplicity of $p$ in the sum $a + b$ equals the multiplicity of $p$ in $b$, i.e., $\text{multiplicity}\, p\, (a + b) = \text{multiplicity}\, p\, b$.

emultiplicity_sub_of_gt theorem

{p a b : α} (h : emultiplicity p b < emultiplicity p a) : emultiplicity p (a - b) = emultiplicity p b

Full source

theorem emultiplicity_sub_of_gt {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
    emultiplicity p (a - b) = emultiplicity p b := by
  rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]; assumption

Extended Multiplicity of Difference When Multiplicities Are Ordered: $\text{emultiplicity}\, p\, (a - b) = \text{emultiplicity}\, p\, b$ if $\text{emultiplicity}\, p\, b < \text{emultiplicity}\, p\, a$

Informal description

For elements $p$, $a$, and $b$ in a commutative monoid $\alpha$, if the extended multiplicity of $p$ in $b$ is strictly less than the extended multiplicity of $p$ in $a$, then the extended multiplicity of $p$ in the difference $a - b$ equals the extended multiplicity of $p$ in $b$, i.e., \[ \text{emultiplicity}\, p\, (a - b) = \text{emultiplicity}\, p\, b. \]

multiplicity_sub_of_gt theorem

 {p a b : α} (h : multiplicity p b < multiplicity p a) (hfin : FiniteMultiplicity p b) :
  multiplicity p (a - b) = multiplicity p b

Full source

theorem multiplicity_sub_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a)
    (hfin : FiniteMultiplicity p b) : multiplicity p (a - b) = multiplicity p b := by
  rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt] <;> rw [multiplicity_neg]; assumption

Multiplicity of Difference When Multiplicities Are Ordered and Finite: $\text{multiplicity}\, p\, (a - b) = \text{multiplicity}\, p\, b$

Informal description

For elements $p$, $a$, and $b$ in a commutative monoid $\alpha$, if the multiplicity of $p$ in $b$ is finite and strictly less than the multiplicity of $p$ in $a$, then the multiplicity of $p$ in the difference $a - b$ equals the multiplicity of $p$ in $b$, i.e., \[ \text{multiplicity}\, p\, (a - b) = \text{multiplicity}\, p\, b. \]

emultiplicity_add_eq_min theorem

 {p a b : α} (h : emultiplicity p a ≠ emultiplicity p b) :
  emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Full source

theorem emultiplicity_add_eq_min {p a b : α}
    (h : emultiplicityemultiplicity p a ≠ emultiplicity p b) :
    emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b) := by
  rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
  · rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab
  · contradiction
  · rw [emultiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

Extended Multiplicity of Sum Equals Minimum When Multiplicities Differ

Informal description

For elements $p$, $a$, and $b$ in a commutative monoid $\alpha$, if the extended multiplicities of $p$ in $a$ and $b$ are distinct, then the extended multiplicity of $p$ in the sum $a + b$ is equal to the minimum of the extended multiplicities of $p$ in $a$ and $b$, i.e., \[ \text{emultiplicity}\, p\, (a + b) = \min(\text{emultiplicity}\, p\, a, \text{emultiplicity}\, p\, b). \]

multiplicity_add_eq_min theorem

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

Full source

theorem multiplicity_add_eq_min {p a b : α} (ha : FiniteMultiplicity p a)
    (hb : FiniteMultiplicity p b) (h : multiplicitymultiplicity p a ≠ multiplicity p b) :
    multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b) := by
  rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
  · rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab
  · contradiction
  · rw [hb.multiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

Multiplicity of Sum Equals Minimum for Distinct Finite Multiplicities

Informal description

For elements $p$, $a$, and $b$ in a commutative monoid $\alpha$, if the multiplicities of $p$ in $a$ and $b$ are finite and distinct, then the multiplicity of $p$ in the sum $a + b$ is equal to the minimum of the multiplicities of $p$ in $a$ and $b$, i.e., \[ \text{multiplicity}\, p\, (a + b) = \min(\text{multiplicity}\, p\, a, \text{multiplicity}\, p\, b). \]

finiteMultiplicity_mul_aux theorem

 {p : α} (hp : Prime p) {a b : α} : ∀ {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b

Full source

theorem finiteMultiplicity_mul_aux {p : α} (hp : Prime p) {a b : α} :
    ∀ {n m : ℕ}, ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
  | n, m => fun ha hb ⟨s, hs⟩ =>
    have : p ∣ a * b := ⟨p ^ (n + m) * s, by simp [hs, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩
    (hp.2.2 a b this).elim
      (fun ⟨x, hx⟩ =>
        have hn0 : 0 < n :=
          Nat.pos_of_ne_zero fun hn0 => by simp [hx, hn0] at ha
        have hpx : ¬p ^ (n - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
          ha (hx.symm ▸ ⟨y, mul_right_cancel₀ hp.1 <| by
            rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy
            simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩)
        have : 1 ≤ n + m := le_trans hn0 (Nat.le_add_right n m)
        finiteMultiplicity_mul_aux hp hpx hb
          ⟨s, mul_right_cancel₀ hp.1 (by
                rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
                simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add])⟩)
      fun ⟨x, hx⟩ =>
        have hm0 : 0 < m :=
          Nat.pos_of_ne_zero fun hm0 => by simp [hx, hm0] at hb
        have hpx : ¬p ^ (m - 1 + 1) ∣ x := fun ⟨y, hy⟩ =>
          hb
            (hx.symm ▸
              ⟨y,
                mul_right_cancel₀ hp.1 <| by
                  rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy
                  simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]⟩)
        finiteMultiplicity_mul_aux hp ha hpx
        ⟨s, mul_right_cancel₀ hp.1 (by
              rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
              simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add])⟩

Non-divisibility of Product by High Powers of a Prime

Informal description

Let $p$ be a prime element in a commutative monoid $\alpha$, and let $a, b \in \alpha$. For any natural numbers $n$ and $m$, if $p^{n+1}$ does not divide $a$ and $p^{m+1}$ does not divide $b$, then $p^{n+m+1}$ does not divide $a \cdot b$.

Prime.finiteMultiplicity_mul theorem

{p a b : α} (hp : Prime p) : FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b)

Full source

theorem Prime.finiteMultiplicity_mul {p a b : α} (hp : Prime p) :
    FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b) :=
  fun ⟨n, hn⟩ ⟨m, hm⟩ => ⟨n + m, finiteMultiplicity_mul_aux hp hn hm⟩

Finite Multiplicity of Product under Prime Element

Informal description

Let $p$ be a prime element in a commutative monoid $\alpha$, and let $a, b \in \alpha$. If the multiplicity of $p$ in $a$ is finite and the multiplicity of $p$ in $b$ is finite, then the multiplicity of $p$ in $a \cdot b$ is also finite.

FiniteMultiplicity.mul_iff theorem

{p a b : α} (hp : Prime p) : FiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b

Full source

theorem FiniteMultiplicity.mul_iff {p a b : α} (hp : Prime p) :
    FiniteMultiplicityFiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b :=
  ⟨fun h => ⟨h.mul_left, h.mul_right⟩, fun h =>
    hp.finiteMultiplicity_mul h.1 h.2⟩

Finite Multiplicity of Product under Prime Element if and only if Finite Multiplicity of Factors

Informal description

For a prime element $p$ in a commutative monoid $\alpha$ and elements $a, b \in \alpha$, the multiplicity of $p$ in the product $a \cdot b$ is finite if and only if the multiplicities of $p$ in both $a$ and $b$ are finite. In other words, $\text{FiniteMultiplicity}\, p\, (a \cdot b) \leftrightarrow \text{FiniteMultiplicity}\, p\, a \land \text{FiniteMultiplicity}\, p\, b$.

FiniteMultiplicity.pow theorem

{p a : α} (hp : Prime p) (hfin : FiniteMultiplicity p a) {k : ℕ} : FiniteMultiplicity p (a ^ k)

Full source

theorem FiniteMultiplicity.pow {p a : α} (hp : Prime p)
    (hfin : FiniteMultiplicity p a) {k : ℕ} : FiniteMultiplicity p (a ^ k) :=
  match k, hfin with
  | 0, _ => ⟨0, by simp [mt isUnit_iff_dvd_one.2 hp.2.1]⟩
  | k + 1, ha => by rw [_root_.pow_succ']; exact hp.finiteMultiplicity_mul ha (ha.pow hp)

Finite Multiplicity is Preserved under Powers for Prime Elements

Informal description

Let $p$ be a prime element in a commutative monoid $\alpha$, and let $a \in \alpha$ have finite multiplicity with respect to $p$. Then for any natural number $k$, the element $a^k$ also has finite multiplicity with respect to $p$.

multiplicity_self theorem

{a : α} : multiplicity a a = 1

Full source

@[simp]
theorem multiplicity_self {a : α} : multiplicity a a = 1 := by
  by_cases ha : FiniteMultiplicity a a
  · rw [ha.multiplicity_eq_iff]
    simp only [pow_one, dvd_refl, reduceAdd, true_and]
    rintro ⟨v, hv⟩
    nth_rw 1 [← mul_one a] at hv
    simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv
    obtain hv | rfl := hv
    · have : IsUnit a := isUnit_of_mul_eq_one a v hv.symm
      simpa [this] using ha.not_unit
    · simpa using ha.ne_zero
  · simp [ha]

Multiplicity of an Element in Itself is One

Informal description

For any element $a$ in a commutative monoid $\alpha$, the multiplicity of $a$ in itself is $1$, i.e., $\text{multiplicity}\, a\, a = 1$.

FiniteMultiplicity.emultiplicity_self theorem

{a : α} (hfin : FiniteMultiplicity a a) : emultiplicity a a = 1

Full source

@[simp]
theorem FiniteMultiplicity.emultiplicity_self {a : α} (hfin : FiniteMultiplicity a a) :
    emultiplicity a a = 1 := by
  simp [hfin.emultiplicity_eq_multiplicity]

Extended Multiplicity of an Element in Itself is One When Finite

Informal description

For any element $a$ in a commutative monoid $\alpha$, if the multiplicity of $a$ in itself is finite (i.e., $\text{FiniteMultiplicity}\, a\, a$ holds), then the extended multiplicity $\text{emultiplicity}\, a\, a$ equals $1$.

multiplicity_mul theorem

 {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) :
  multiplicity p (a * b) = multiplicity p a + multiplicity p b

Full source

theorem multiplicity_mul {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) :
    multiplicity p (a * b) = multiplicity p a + multiplicity p b := by
  have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
  have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
  have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
    rw [pow_add]; apply mul_dvd_mul <;> assumption
  have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
    fun h =>
    not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
  rw [hfin.multiplicity_eq_iff]
  exact ⟨hdiv, hsucc⟩

Additivity of Multiplicity for Prime Elements: $\text{multiplicity}\, p\, (a \cdot b) = \text{multiplicity}\, p\, a + \text{multiplicity}\, p\, b$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$ and elements $a, b \in \alpha$ such that the multiplicity of $p$ in $a \cdot b$ is finite, the multiplicity of $p$ in the product $a \cdot b$ is equal to the sum of the multiplicities of $p$ in $a$ and $p$ in $b$, i.e., \[ \text{multiplicity}\, p\, (a \cdot b) = \text{multiplicity}\, p\, a + \text{multiplicity}\, p\, b. \]

emultiplicity_mul theorem

{p a b : α} (hp : Prime p) : emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Full source

theorem emultiplicity_mul {p a b : α} (hp : Prime p) :
    emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b := by
  by_cases hfin : FiniteMultiplicity p (a * b)
  · rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]
    norm_cast
    exact multiplicity_mul hp hfin
  · rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]
    simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

Additivity of Extended Multiplicity for Prime Elements: $\text{emultiplicity}\, p\, (a \cdot b) = \text{emultiplicity}\, p\, a + \text{emultiplicity}\, p\, b$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$ and elements $a, b \in \alpha$, the extended multiplicity of $p$ in the product $a \cdot b$ is equal to the sum of the extended multiplicities of $p$ in $a$ and $p$ in $b$, i.e., \[ \text{emultiplicity}\, p\, (a \cdot b) = \text{emultiplicity}\, p\, a + \text{emultiplicity}\, p\, b. \]

Finset.emultiplicity_prod theorem

 {β : Type*} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) :
  emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Full source

theorem Finset.emultiplicity_prod {β : Type*} {p : α} (hp : Prime p) (s : Finset β) (f : β → α) :
    emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x) := by classical
    induction' s using Finset.induction with a s has ih h
    · simp only [Finset.sum_empty, Finset.prod_empty]
      exact emultiplicity_of_one_right hp.not_unit
    · simpa [has, ← ih] using emultiplicity_mul hp

Additivity of Extended Multiplicity for Products over Finite Sets: $\text{emultiplicity}\, p\, \left(\prod_{x \in s} f(x)\right) = \sum_{x \in s} \text{emultiplicity}\, p\, (f(x))$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$, any finite set $s$ with elements of type $\beta$, and any function $f \colon \beta \to \alpha$, the extended multiplicity of $p$ in the product $\prod_{x \in s} f(x)$ is equal to the sum over $x \in s$ of the extended multiplicities of $p$ in $f(x)$, i.e., \[ \text{emultiplicity}\, p\, \left(\prod_{x \in s} f(x)\right) = \sum_{x \in s} \text{emultiplicity}\, p\, (f(x)). \]

emultiplicity_pow theorem

{p a : α} (hp : Prime p) {k : ℕ} : emultiplicity p (a ^ k) = k * emultiplicity p a

Full source

theorem emultiplicity_pow {p a : α} (hp : Prime p) {k : ℕ} :
    emultiplicity p (a ^ k) = k * emultiplicity p a := by
  induction' k with k hk
  · simp [emultiplicity_of_one_right hp.not_unit]
  · simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

Extended Multiplicity of Power: $\text{emultiplicity}\, p\, (a^k) = k \cdot \text{emultiplicity}\, p\, a$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$ and any element $a \in \alpha$, the extended multiplicity of $p$ in $a^k$ is equal to $k$ times the extended multiplicity of $p$ in $a$, i.e., \[ \text{emultiplicity}\, p\, (a^k) = k \cdot \text{emultiplicity}\, p\, a. \]

FiniteMultiplicity.multiplicity_pow theorem

{p a : α} (hp : Prime p) (ha : FiniteMultiplicity p a) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a

Full source

protected theorem FiniteMultiplicity.multiplicity_pow {p a : α} (hp : Prime p)
    (ha : FiniteMultiplicity p a) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a := by
  exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸
    ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp

Multiplicativity of Multiplicity for Powers: $\text{multiplicity}\, p\, (a^k) = k \cdot \text{multiplicity}\, p\, a$

Informal description

Let $p$ be a prime element in a commutative monoid $\alpha$, and let $a \in \alpha$ have finite multiplicity with respect to $p$. Then for any natural number $k$, the multiplicity of $p$ in $a^k$ is equal to $k$ times the multiplicity of $p$ in $a$, i.e., \[ \text{multiplicity}\, p\, (a^k) = k \cdot \text{multiplicity}\, p\, a. \]

emultiplicity_pow_self theorem

{p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : emultiplicity p (p ^ n) = n

Full source

theorem emultiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) :
    emultiplicity p (p ^ n) = n := by
  apply emultiplicity_eq_of_dvd_of_not_dvd
  · rfl
  · rw [pow_dvd_pow_iff h0 hu]
    apply Nat.not_succ_le_self

Extended multiplicity of a power equals its exponent for non-zero non-units

Informal description

For any element $p$ in a commutative monoid $\alpha$ such that $p$ is neither zero nor a unit, and for any natural number $n$, the extended multiplicity of $p$ in $p^n$ is equal to $n$, i.e., $\text{emultiplicity}\, p\, (p^n) = n$.

multiplicity_pow_self theorem

{p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : multiplicity p (p ^ n) = n

Full source

theorem multiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) :
    multiplicity p (p ^ n) = n :=
  multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_pow_self h0 hu n)

Multiplicity of a Power Equals its Exponent for Non-zero Non-units

Informal description

For any element $p$ in a commutative monoid $\alpha$ such that $p$ is neither zero nor a unit, and for any natural number $n$, the multiplicity of $p$ in $p^n$ is equal to $n$, i.e., $\text{multiplicity}\, p\, (p^n) = n$.

emultiplicity_pow_self_of_prime theorem

{p : α} (hp : Prime p) (n : ℕ) : emultiplicity p (p ^ n) = n

Full source

theorem emultiplicity_pow_self_of_prime {p : α} (hp : Prime p) (n : ℕ) :
    emultiplicity p (p ^ n) = n :=
  emultiplicity_pow_self hp.ne_zero hp.not_unit n

Extended multiplicity of a prime power equals its exponent: $\text{emultiplicity}\, p\, (p^n) = n$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$ and any natural number $n$, the extended multiplicity of $p$ in $p^n$ is equal to $n$, i.e., $\text{emultiplicity}\, p\, (p^n) = n$.

multiplicity_pow_self_of_prime theorem

{p : α} (hp : Prime p) (n : ℕ) : multiplicity p (p ^ n) = n

Full source

theorem multiplicity_pow_self_of_prime {p : α} (hp : Prime p) (n : ℕ) :
    multiplicity p (p ^ n) = n :=
  multiplicity_pow_self hp.ne_zero hp.not_unit n

Multiplicity of Prime Power Equals Exponent: $\text{multiplicity}(p, p^n) = n$

Informal description

For any prime element $p$ in a commutative monoid $\alpha$ and any natural number $n$, the multiplicity of $p$ in $p^n$ is equal to $n$, i.e., $\text{multiplicity}(p, p^n) = n$.

multiplicity_eq_zero_of_coprime theorem

 {p a b : ℕ} (hp : p ≠ 1) (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.Coprime a b) : multiplicity p a = 0

Full source

theorem multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1)
    (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.Coprime a b) : multiplicity p a = 0 := by
  apply Nat.eq_zero_of_not_pos
  intro nh
  have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
  have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
  have := Nat.dvd_gcd da db
  rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this
  exact hp this

Multiplicity Zero for Coprime Numbers with Prime Power Condition

Informal description

For natural numbers $p$, $a$, and $b$ with $p \neq 1$, if the multiplicity of $p$ in $a$ is less than or equal to its multiplicity in $b$, and $a$ and $b$ are coprime, then the multiplicity of $p$ in $a$ is zero.

Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs theorem

{a b : ℤ} : FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Full source

theorem Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} :
    FiniteMultiplicityFiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs := by
  simp only [FiniteMultiplicity.def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]

Equivalence of Finite Multiplicity for Integers and Their Absolute Values

Informal description

For any integers $a$ and $b$, the multiplicity of $a$ as a divisor of $b$ is finite if and only if the multiplicity of $|a|$ as a divisor of $|b|$ is finite in the natural numbers. In other words, $\text{FiniteMultiplicity}(a, b) \leftrightarrow \text{FiniteMultiplicity}(|a|, |b|)$.

Int.finiteMultiplicity_iff theorem

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

Full source

theorem Int.finiteMultiplicity_iff {a b : ℤ} : FiniteMultiplicityFiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0 := by
  rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]

Finite Multiplicity Criterion for Integers: $|a| \neq 1$ and $b \neq 0$

Informal description

For any integers $a$ and $b$, the multiplicity of $a$ as a divisor of $b$ is finite if and only if the absolute value of $a$ is not equal to $1$ and $b$ is not equal to $0$. In other words, $\text{FiniteMultiplicity}(a, b) \leftrightarrow (|a| \neq 1 \land b \neq 0)$.

Nat.decidableFiniteMultiplicity instance

: DecidableRel fun a b : ℕ => FiniteMultiplicity a b

Full source

instance Nat.decidableFiniteMultiplicity : DecidableRel fun a b : ℕ => FiniteMultiplicity a b :=
  fun _ _ ↦ decidable_of_iff' _ Nat.finiteMultiplicity_iff

Decidability of Finite Multiplicity for Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the predicate $\text{FiniteMultiplicity}\, a\, b$ is decidable.

Int.decidableMultiplicityFinite instance

: DecidableRel fun a b : ℤ => FiniteMultiplicity a b

Full source

instance Int.decidableMultiplicityFinite : DecidableRel fun a b : ℤ => FiniteMultiplicity a b :=
  fun _ _ ↦ decidable_of_iff' _ Int.finiteMultiplicity_iff

Decidability of Finite Multiplicity for Integers

Informal description

For any integers $a$ and $b$, the predicate $\text{FiniteMultiplicity}\, a\, b$ is decidable. That is, there exists an algorithm to determine whether the multiplicity of $a$ as a divisor of $b$ is finite.

Main definitions