Documentation

Mathlib.RingTheory.Multiplicity

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 #

@[reducible, inline]
abbrev FiniteMultiplicity {α : Type u_1} [Monoid α] (a b : α) :

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

Equations
    Instances For
      @[deprecated FiniteMultiplicity (since := "2024-11-30")]
      def multiplicity.Finite {α : Type u_1} [Monoid α] (a b : α) :

      Alias of FiniteMultiplicity.


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

      Equations
        Instances For
          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
            Instances For
              noncomputable def multiplicity {α : Type u_1} [Monoid α] (a b : α) :

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

              Equations
                Instances For
                  @[simp]
                  theorem emultiplicity_eq_top {α : Type u_1} [Monoid α] {a b : α} :
                  theorem emultiplicity_lt_top {α : Type u_1} [Monoid α] {a b : α} :
                  @[deprecated finiteMultiplicity_iff_emultiplicity_ne_top (since := "2024-11-30")]

                  Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

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

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

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

                  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) :
                  theorem emultiplicity_ne_of_multiplicity_ne {α : Type u_1} [Monoid α] {a b : α} {n : } :
                  multiplicity a b nemultiplicity a b n
                  @[deprecated FiniteMultiplicity.emultiplicity_eq_multiplicity (since := "2024-11-30")]

                  Alias of FiniteMultiplicity.emultiplicity_eq_multiplicity.

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

                  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) :
                  @[simp]
                  @[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) :

                  Alias of multiplicity_eq_one_of_not_finiteMultiplicity.

                  @[simp]
                  theorem multiplicity_le_emultiplicity {α : Type u_1} [Monoid α] {a b : α} :
                  theorem multiplicity_eq_of_emultiplicity_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] {a b : α} {c d : β} (h : emultiplicity a b = emultiplicity c d) :
                  theorem multiplicity_le_of_emultiplicity_le {α : Type u_1} [Monoid α] {a b : α} {n : } (h : emultiplicity 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) :
                  @[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) :

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

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

                  Alias of FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity.

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

                  @[deprecated FiniteMultiplicity.not_dvd_of_one_right (since := "2024-11-30")]
                  theorem multiplicity.Finite.not_dvd_of_one_right {α : Type u_1} [Monoid α] {a : α} :

                  Alias of FiniteMultiplicity.not_dvd_of_one_right.

                  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) :
                  @[deprecated FiniteMultiplicity.not_unit (since := "2024-11-30")]
                  theorem multiplicity.Finite.not_unit {α : Type u_1} [Monoid α] {a b : α} (h : FiniteMultiplicity a b) :

                  Alias of FiniteMultiplicity.not_unit.

                  theorem FiniteMultiplicity.mul_left {α : Type u_1} [Monoid α] {a b c : α} :
                  @[deprecated FiniteMultiplicity.mul_left (since := "2024-11-30")]
                  theorem multiplicity.Finite.mul_left {α : Type u_1} [Monoid α] {a b c : α} :

                  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 : α) :
                  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) :
                  theorem emultiplicity_pos_of_dvd {α : Type u_1} [Monoid α] {a b : α} (hdiv : 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) :
                  theorem le_emultiplicity_of_pow_dvd {α : Type u_1} [Monoid α] {a b : α} {k : } (hk : a ^ k b) :
                  theorem FiniteMultiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [Monoid α] {a b : α} (hf : FiniteMultiplicity a b) {k : } (hk : a ^ k 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) :

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

                  Alias of FiniteMultiplicity.not_of_isUnit_left.

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

                  Alias of FiniteMultiplicity.not_of_one_left.

                  @[simp]
                  theorem emultiplicity_one_left {α : Type u_1} [Monoid α] (b : α) :
                  @[simp]
                  theorem FiniteMultiplicity.one_right {α : Type u_1} [Monoid α] {a : α} (ha : FiniteMultiplicity a 1) :
                  @[deprecated FiniteMultiplicity.one_right (since := "2024-11-30")]
                  theorem multiplicity.Finite.one_right {α : Type u_1} [Monoid α] {a : α} (ha : FiniteMultiplicity a 1) :

                  Alias of FiniteMultiplicity.one_right.

                  theorem FiniteMultiplicity.not_of_unit_left {α : Type u_1} [Monoid α] (a : α) (u : αˣ) :
                  @[deprecated FiniteMultiplicity.not_of_unit_left (since := "2024-11-30")]
                  theorem multiplicity.Finite.not_of_unit_left {α : Type u_1} [Monoid α] (a : α) (u : αˣ) :

                  Alias of FiniteMultiplicity.not_of_unit_left.

                  theorem emultiplicity_eq_zero {α : Type u_1} [Monoid α] {a b : α} :
                  theorem multiplicity_eq_zero {α : Type u_1} [Monoid α] {a b : α} :
                  theorem emultiplicity_ne_zero {α : Type u_1} [Monoid α] {a b : α} :
                  theorem multiplicity_ne_zero {α : Type u_1} [Monoid α] {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 bc ^ 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 bc ^ 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 bc ^ 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 : α} :
                  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) :
                  theorem emultiplicity_eq_of_associated_right {α : Type u_1} [Monoid α] {a b c : α} (h : Associated b c) :
                  theorem multiplicity_eq_of_associated_right {α : Type u_1} [Monoid α] {a b c : α} (h : Associated b 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 : α} :
                  @[deprecated Nat.finiteMultiplicity_iff (since := "2024-11-30")]

                  Alias of Nat.finiteMultiplicity_iff.

                  theorem Dvd.multiplicity_pos {α : Type u_1} [Monoid α] {a b : α} :
                  a b0 < 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)) :
                  @[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)) :

                  Alias of FiniteMultiplicity.mul_right.

                  theorem emultiplicity_of_isUnit_right {α : Type u_1} [CommMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : IsUnit b) :
                  theorem multiplicity_of_isUnit_right {α : Type u_1} [CommMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : IsUnit b) :
                  theorem emultiplicity_of_one_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) :
                  theorem multiplicity_of_one_right {α : Type u_1} [CommMonoid α] {a : α} (ha : ¬IsUnit a) :
                  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) :
                  theorem emultiplicity_eq_of_associated_left {α : Type u_1} [CommMonoid α] {a b c : α} (h : Associated a b) :
                  theorem multiplicity_eq_of_associated_left {α : Type u_1} [CommMonoid α] {a b c : α} (h : Associated 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 : α) :
                  @[simp]
                  theorem emultiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] (a : α) (ha : a 0) :
                  @[simp]
                  theorem multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] (a : α) (ha : a 0) :
                  @[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)) :

                  Alias of FiniteMultiplicity.or_of_add.

                  theorem min_le_emultiplicity_add {α : Type u_1} [Semiring α] {p a b : α} :
                  @[simp]
                  theorem FiniteMultiplicity.neg_iff {α : Type u_1} [Ring α] {a b : α} :
                  @[deprecated FiniteMultiplicity.neg_iff (since := "2024-11-30")]
                  theorem multiplicity.Finite.neg_iff {α : Type u_1} [Ring α] {a b : α} :

                  Alias of FiniteMultiplicity.neg_iff.

                  theorem FiniteMultiplicity.neg {α : Type u_1} [Ring α] {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 : α} :

                  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 : α) :
                  @[simp]
                  theorem multiplicity_neg {α : Type u_1} [Ring α] (a b : α) :
                  theorem emultiplicity_add_of_gt {α : Type u_1} [Ring α] {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
                  theorem FiniteMultiplicity.multiplicity_add_of_gt {α : Type u_1} [Ring α] {p a b : α} (hf : FiniteMultiplicity p b) (h : multiplicity p b < multiplicity p a) :
                  @[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) :

                  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) :
                  theorem multiplicity_sub_of_gt {α : Type u_1} [Ring α] {p a b : α} (h : multiplicity p b < multiplicity p a) (hfin : FiniteMultiplicity p b) :
                  theorem emultiplicity_add_eq_min {α : Type u_1} [Ring α] {p a b : α} (h : 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) :
                  @[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.

                  @[deprecated Prime.finiteMultiplicity_mul (since := "2024-11-30")]
                  theorem Prime.multiplicity_finite_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p a b : α} (hp : Prime p) :

                  Alias of Prime.finiteMultiplicity_mul.

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

                  Alias of FiniteMultiplicity.mul_iff.

                  theorem FiniteMultiplicity.pow {α : Type u_1} [CancelCommMonoidWithZero α] {p a : α} (hp : Prime p) (hfin : 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 : } :

                  Alias of FiniteMultiplicity.pow.

                  @[simp]
                  theorem multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} :
                  @[deprecated FiniteMultiplicity.emultiplicity_self (since := "2024-11-30")]

                  Alias of FiniteMultiplicity.emultiplicity_self.

                  theorem multiplicity_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) :
                  theorem emultiplicity_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p a b : α} (hp : Prime p) :
                  theorem Finset.emultiplicity_prod {α : Type u_1} [CancelCommMonoidWithZero α] {β : Type u_3} {p : α} (hp : Prime p) (s : Finset β) (f : βα) :
                  emultiplicity p (∏ xs, f x) = xs, 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) :
                  @[deprecated Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs (since := "2024-11-30")]

                  Alias of Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs.

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

                  Alias of Int.finiteMultiplicity_iff.

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

                  Alias of Nat.decidableFiniteMultiplicity.

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

                      Alias of Int.decidableMultiplicityFinite.

                      Equations
                        Instances For