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

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

Equations
Instances For
    @[deprecated FiniteMultiplicity]
    def multiplicity.Finite {α : Type u_1} [Monoid α] (a b : α) :

    Alias of FiniteMultiplicity.


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

          Alias of finiteMultiplicity_iff_emultiplicity_ne_top.

          @[deprecated FiniteMultiplicity.emultiplicity_ne_top]

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

          Alias of FiniteMultiplicity.emultiplicity_eq_multiplicity.

          @[deprecated FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq]

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

          Alias of FiniteMultiplicity.not_dvd_of_one_right.

          @[deprecated Int.natCast_multiplicity]
          theorem Int.coe_nat_multiplicity (a b : ) :

          Alias of Int.natCast_multiplicity.

          theorem FiniteMultiplicity.not_iff_forall {α : Type u_1} [Monoid α] {a b : α} :
          ¬FiniteMultiplicity a b ∀ (n : ), a ^ n b
          @[deprecated FiniteMultiplicity.not_iff_forall]
          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]
          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]
          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]
          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]
          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]
          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]
          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]
          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]
          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]

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

          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]
          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]
          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]
          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]
          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]
          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 Int.emultiplicity_natAbs (a : ) (b : ) :
          emultiplicity a b.natAbs = emultiplicity (↑a) b
          theorem Int.multiplicity_natAbs (a : ) (b : ) :
          multiplicity a b.natAbs = multiplicity (↑a) b
          theorem emultiplicity_add_of_gt {α : Type u_1} [Ring α] {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
          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]
          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]
          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]
          theorem Prime.multiplicity_finite_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p a b : α} (hp : Prime p) :

          Alias of Prime.finiteMultiplicity_mul.

          @[deprecated FiniteMultiplicity.mul_iff]

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

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

          Alias of Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs.

          @[deprecated Int.finiteMultiplicity_iff]
          theorem Int.multiplicity_finite_iff {a b : } :
          FiniteMultiplicity a b a.natAbs 1 b 0

          Alias of Int.finiteMultiplicity_iff.

          Equations
          Equations