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 #

def multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (b : α) :

multiplicity a b returns the largest natural number n such that a ^ n ∣ b, as a PartENat or natural with infinity. If ∀ n, a ^ n ∣ b, then it returns

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

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

    Equations
    Instances For
      theorem multiplicity.finite_iff_dom {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.finite_def {α : Type u_1} [Monoid α] {a : α} {b : α} :
      multiplicity.Finite a b ∃ (n : ), ¬a ^ (n + 1) b
      theorem multiplicity.not_finite_iff_forall {α : Type u_1} [Monoid α] {a : α} {b : α} :
      ¬multiplicity.Finite a b ∀ (n : ), a ^ n b
      theorem multiplicity.not_unit_of_finite {α : Type u_1} [Monoid α] {a : α} {b : α} (h : multiplicity.Finite a b) :
      theorem multiplicity.finite_of_finite_mul_right {α : Type u_1} [Monoid α] {a : α} {b : α} {c : α} :
      theorem multiplicity.pow_dvd_of_le_multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
      k multiplicity a ba ^ k b
      theorem multiplicity.pow_multiplicity_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (h : multiplicity.Finite a b) :
      a ^ (multiplicity a b).get h b
      theorem multiplicity.is_greatest {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {m : } (hm : multiplicity a b < m) :
      ¬a ^ m b
      theorem multiplicity.is_greatest' {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {m : } (h : multiplicity.Finite a b) (hm : (multiplicity a b).get h < m) :
      ¬a ^ m b
      theorem multiplicity.pos_of_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (hfin : multiplicity.Finite a b) (hdiv : a b) :
      0 < (multiplicity a b).get hfin
      theorem multiplicity.unique {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
      k = multiplicity a b
      theorem multiplicity.unique' {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) (hsucc : ¬a ^ (k + 1) b) :
      k = (multiplicity a b).get
      theorem multiplicity.le_multiplicity_of_pow_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } (hk : a ^ k b) :
      k multiplicity a b
      theorem multiplicity.pow_dvd_iff_le_multiplicity {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
      a ^ k b k multiplicity a b
      theorem multiplicity.multiplicity_lt_iff_not_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {k : } :
      multiplicity a b < k ¬a ^ k b
      theorem multiplicity.eq_coe_iff {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {n : } :
      multiplicity a b = n a ^ n b ¬a ^ (n + 1) b
      theorem multiplicity.eq_top_iff {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      multiplicity a b = ∀ (n : ), a ^ n b
      @[simp]
      theorem multiplicity.isUnit_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (b : α) (ha : IsUnit a) :
      theorem multiplicity.one_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] (b : α) :
      @[simp]
      theorem multiplicity.get_one_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : multiplicity.Finite a 1) :
      (multiplicity a 1).get ha = 0
      theorem multiplicity.unit_left {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (u : αˣ) :
      multiplicity (u) a =
      theorem multiplicity.multiplicity_eq_zero {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.multiplicity_ne_zero {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.eq_top_iff_not_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.ne_top_iff_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.lt_top_iff_finite {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.exists_eq_pow_mul_and_not_dvd {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (hfin : multiplicity.Finite a b) :
      ∃ (c : α), b = a ^ (multiplicity a b).get hfin * c ¬a c
      theorem multiplicity.multiplicity_le_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {a : α} {b : α} {c : β} {d : β} :
      multiplicity a b multiplicity c d ∀ (n : ), a ^ n bc ^ n d
      theorem multiplicity.multiplicity_eq_multiplicity_iff {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {a : α} {b : α} {c : β} {d : β} :
      multiplicity a b = multiplicity c d ∀ (n : ), a ^ n b c ^ n d
      theorem multiplicity.le_multiplicity_map {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {F : Type u_3} [FunLike F α β] [MonoidHomClass F α β] (f : F) {a : α} {b : α} :
      multiplicity a b multiplicity (f a) (f b)
      theorem multiplicity.multiplicity_map_eq {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : β) => x x_1] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] (f : F) {a : α} {b : α} :
      multiplicity (f a) (f b) = multiplicity a b
      theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : b c) :
      theorem multiplicity.eq_of_associated_right {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : Associated b c) :
      theorem multiplicity.dvd_of_multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (h : 0 < multiplicity a b) :
      a b
      theorem multiplicity.dvd_iff_multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      0 < multiplicity a b a b
      theorem has_dvd.dvd.multiplicity_pos {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      a b0 < multiplicity a b

      Alias of the reverse direction of multiplicity.dvd_iff_multiplicity_pos.

      theorem multiplicity.finite_of_finite_mul_left {α : Type u_1} [CommMonoid α] {a : α} {b : α} {c : α} :
      theorem multiplicity.isUnit_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} (ha : ¬IsUnit a) (hb : IsUnit b) :
      theorem multiplicity.one_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬IsUnit a) :
      theorem multiplicity.unit_right {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬IsUnit a) (u : αˣ) :
      multiplicity a u = 0
      theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (hdvd : a b) :
      theorem multiplicity.eq_of_associated_left {α : Type u_1} [CommMonoid α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (h : Associated a b) :
      theorem multiplicity.ne_zero_of_finite {α : Type u_1} [MonoidWithZero α] {a : α} {b : α} (h : multiplicity.Finite a b) :
      b 0
      @[simp]
      theorem multiplicity.zero {α : Type u_1} [MonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) :
      @[simp]
      theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero {α : Type u_1} [MonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (ha : a 0) :
      theorem multiplicity.multiplicity_mk_eq_multiplicity {α : Type u_1} [CommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : Associates α) => x x_1] {a : α} {b : α} :
      theorem multiplicity.min_le_multiplicity_add {α : Type u_1} [Semiring α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} :
      @[simp]
      theorem multiplicity.neg {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x x_1] (a : α) (b : α) :
      theorem multiplicity.multiplicity_add_of_gt {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (h : multiplicity p b < multiplicity p a) :
      theorem multiplicity.multiplicity_sub_of_gt {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (h : multiplicity p b < multiplicity p a) :
      theorem multiplicity.multiplicity_add_eq_min {α : Type u_1} [Ring α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (h : multiplicity p a multiplicity p b) :
      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
      theorem multiplicity.finite_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} (hp : Prime p) :
      theorem multiplicity.finite_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {a : α} (hp : Prime p) {k : } :
      @[simp]
      theorem multiplicity.multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : ¬IsUnit a) (ha0 : a 0) :
      @[simp]
      theorem multiplicity.get_multiplicity_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {a : α} (ha : multiplicity.Finite a a) :
      (multiplicity a a).get ha = 1
      theorem multiplicity.mul' {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (hp : Prime p) (h : (multiplicity p (a * b)).Dom) :
      (multiplicity p (a * b)).get h = (multiplicity p a).get + (multiplicity p b).get
      theorem multiplicity.mul {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} {b : α} (hp : Prime p) :
      theorem multiplicity.Finset.prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {β : Type u_3} {p : α} (hp : Prime p) (s : Finset β) (f : βα) :
      multiplicity p (Finset.prod s fun (x : β) => f x) = Finset.sum s fun (x : β) => multiplicity p (f x)
      theorem multiplicity.pow' {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} (hp : Prime p) (ha : multiplicity.Finite p a) {k : } :
      (multiplicity p (a ^ k)).get = k * (multiplicity p a).get ha
      theorem multiplicity.pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} {a : α} (hp : Prime p) {k : } :
      theorem multiplicity.multiplicity_pow_self {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {p : α} (h0 : p 0) (hu : ¬IsUnit p) (n : ) :
      multiplicity p (p ^ n) = n
      theorem multiplicity.multiplicity_pow_self_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableRel fun (x x_1 : α) => x x_1] {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 : Nat.Coprime a b) :