Documentation

Mathlib.Algebra.Associated.Basic

Associated, prime, and irreducible elements. #

In this file we define the predicate Prime p saying that an element of a commutative monoid with zero is prime. Namely, Prime p means that p isn't zero, it isn't a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;

In decomposition monoids (e.g., , ), this predicate is equivalent to Irreducible, however this is not true in general.

We also define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient.

def Prime {M : Type u_1} [CommMonoidWithZero M] (p : M) :

An element p of a commutative monoid with zero (e.g., a ring) is called prime, if it's not zero, not a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b.

Equations
Instances For
    theorem Prime.ne_zero {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
    p 0
    theorem Prime.not_unit {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
    theorem Prime.not_dvd_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
    ¬p 1
    theorem Prime.ne_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
    p 1
    theorem Prime.dvd_or_dvd {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {b : M} (h : p a * b) :
    p a p b
    theorem Prime.dvd_mul {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {b : M} :
    p a * b p a p b
    theorem Prime.isPrimal {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
    theorem Prime.not_dvd_mul {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {b : M} (ha : ¬p a) (hb : ¬p b) :
    ¬p a * b
    theorem Prime.dvd_of_dvd_pow {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {n : } (h : p a ^ n) :
    p a
    theorem Prime.dvd_pow_iff_dvd {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {n : } (hn : n 0) :
    p a ^ n p a
    @[simp]
    @[simp]
    theorem not_prime_one {M : Type u_1} [CommMonoidWithZero M] :
    theorem comap_prime {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {F : Type u_3} {G : Type u_4} [FunLike F M N] [MonoidWithZeroHomClass F M N] [FunLike G N M] [MulHomClass G N M] (f : F) (g : G) {p : M} (hinv : ∀ (a : M), g (f a) = a) (hp : Prime (f p)) :
    theorem MulEquiv.prime_iff {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {p : M} (e : M ≃* N) :
    Prime p Prime (e p)
    theorem Prime.left_dvd_or_dvd_right_of_dvd_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {b : M} :
    a p * bp a a b
    theorem Prime.pow_dvd_of_dvd_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {a : M} {b : M} (hp : Prime p) (n : ) (h : ¬p a) (h' : p ^ n a * b) :
    p ^ n b
    theorem Prime.pow_dvd_of_dvd_mul_right {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {a : M} {b : M} (hp : Prime p) (n : ) (h : ¬p b) (h' : p ^ n a * b) :
    p ^ n a
    theorem Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {a : M} {b : M} {n : } (hp : Prime p) (hpow : p ^ n.succ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 b) :
    p a
    theorem prime_pow_succ_dvd_mul {M : Type u_3} [CancelCommMonoidWithZero M] {p : M} {x : M} {y : M} (h : Prime p) {i : } (hxy : p ^ (i + 1) x * y) :
    p ^ (i + 1) x p y
    structure Irreducible {M : Type u_1} [Monoid M] (p : M) :

    Irreducible p states that p is non-unit and only factors into units.

    We explicitly avoid stating that p is non-zero, this would require a semiring. Assuming only a monoid allows us to reuse irreducible for associated elements.

    • not_unit : ¬IsUnit p

      p is not a unit

    • isUnit_or_isUnit' : ∀ (a b : M), p = a * bIsUnit a IsUnit b

      if p factors then one factor is a unit

    Instances For
      theorem Irreducible.not_unit {M : Type u_1} [Monoid M] {p : M} (self : Irreducible p) :

      p is not a unit

      theorem Irreducible.isUnit_or_isUnit' {M : Type u_1} [Monoid M] {p : M} (self : Irreducible p) (a : M) (b : M) :
      p = a * bIsUnit a IsUnit b

      if p factors then one factor is a unit

      theorem Irreducible.not_dvd_one {M : Type u_1} [CommMonoid M] {p : M} (hp : Irreducible p) :
      ¬p 1
      theorem Irreducible.isUnit_or_isUnit {M : Type u_1} [Monoid M] {p : M} (hp : Irreducible p) {a : M} {b : M} (h : p = a * b) :
      theorem irreducible_iff {M : Type u_1} [Monoid M] {p : M} :
      Irreducible p ¬IsUnit p ∀ (a b : M), p = a * bIsUnit a IsUnit b
      @[simp]
      theorem not_irreducible_one {M : Type u_1} [Monoid M] :
      theorem Irreducible.ne_one {M : Type u_1} [Monoid M] {p : M} :
      Irreducible pp 1
      theorem Irreducible.ne_zero {M : Type u_1} [MonoidWithZero M] {p : M} :
      Irreducible pp 0
      theorem of_irreducible_mul {M : Type u_3} [Monoid M] {x : M} {y : M} :
      Irreducible (x * y)IsUnit x IsUnit y
      theorem not_irreducible_pow {M : Type u_3} [Monoid M] {x : M} {n : } (hn : n 1) :
      theorem irreducible_or_factor {M : Type u_3} [Monoid M] (x : M) (h : ¬IsUnit x) :
      Irreducible x ∃ (a : M), ∃ (b : M), ¬IsUnit a ¬IsUnit b a * b = x
      theorem Irreducible.dvd_symm {M : Type u_1} [Monoid M] {p : M} {q : M} (hp : Irreducible p) (hq : Irreducible q) :
      p qq p

      If p and q are irreducible, then p ∣ q implies q ∣ p.

      theorem Irreducible.dvd_comm {M : Type u_1} [Monoid M] {p : M} {q : M} (hp : Irreducible p) (hq : Irreducible q) :
      p q q p
      theorem irreducible_units_mul {M : Type u_1} [Monoid M] (a : Mˣ) (b : M) :
      theorem irreducible_isUnit_mul {M : Type u_1} [Monoid M] {a : M} {b : M} (h : IsUnit a) :
      theorem irreducible_mul_units {M : Type u_1} [Monoid M] (a : Mˣ) (b : M) :
      theorem irreducible_mul_isUnit {M : Type u_1} [Monoid M] {a : M} {b : M} (h : IsUnit a) :
      theorem irreducible_mul_iff {M : Type u_1} [Monoid M] {a : M} {b : M} :
      theorem Irreducible.not_square {M : Type u_1} [CommMonoid M] {a : M} (ha : Irreducible a) :
      theorem IsSquare.not_irreducible {M : Type u_1} [CommMonoid M] {a : M} (ha : IsSquare a) :
      theorem Irreducible.prime_of_isPrimal {M : Type u_1} [CommMonoidWithZero M] {a : M} (irr : Irreducible a) (primal : IsPrimal a) :
      theorem Prime.irreducible {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) :
      theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {b : M} {k : } {l : } :
      p ^ k ap ^ l bp ^ (k + l + 1) a * bp ^ (k + 1) a p ^ (l + 1) b
      theorem Prime.not_square {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) :
      theorem IsSquare.not_prime {M : Type u_1} [CancelCommMonoidWithZero M] {a : M} (ha : IsSquare a) :
      theorem not_prime_pow {M : Type u_1} [CancelCommMonoidWithZero M] {a : M} {n : } (hn : n 1) :
      ¬Prime (a ^ n)
      def Associated {M : Type u_1} [Monoid M] (x : M) (y : M) :

      Two elements of a Monoid are Associated if one of them is another one multiplied by a unit on the right.

      Equations
      Instances For
        theorem Associated.refl {M : Type u_1} [Monoid M] (x : M) :
        theorem Associated.rfl {M : Type u_1} [Monoid M] {x : M} :
        instance Associated.instIsRefl {M : Type u_1} [Monoid M] :
        IsRefl M Associated
        Equations
        • =
        theorem Associated.symm {M : Type u_1} [Monoid M] {x : M} {y : M} :
        instance Associated.instIsSymm {M : Type u_1} [Monoid M] :
        IsSymm M Associated
        Equations
        • =
        theorem Associated.comm {M : Type u_1} [Monoid M] {x : M} {y : M} :
        theorem Associated.trans {M : Type u_1} [Monoid M] {x : M} {y : M} {z : M} :
        Associated x yAssociated y zAssociated x z
        instance Associated.instIsTrans {M : Type u_1} [Monoid M] :
        IsTrans M Associated
        Equations
        • =
        def Associated.setoid (M : Type u_3) [Monoid M] :

        The setoid of the relation x ~ᵤ y iff there is a unit u such that x * u = y

        Equations
        Instances For
          theorem Associated.map {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {F : Type u_5} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x : M} {y : M} (ha : Associated x y) :
          Associated (f x) (f y)
          theorem unit_associated_one {M : Type u_1} [Monoid M] {u : Mˣ} :
          Associated (↑u) 1
          @[simp]
          theorem associated_one_iff_isUnit {M : Type u_1} [Monoid M] {a : M} :
          @[simp]
          theorem associated_zero_iff_eq_zero {M : Type u_1} [MonoidWithZero M] (a : M) :
          Associated a 0 a = 0
          theorem associated_one_of_mul_eq_one {M : Type u_1} [CommMonoid M] {a : M} (b : M) (hab : a * b = 1) :
          theorem associated_one_of_associated_mul_one {M : Type u_1} [CommMonoid M] {a : M} {b : M} :
          Associated (a * b) 1Associated a 1
          theorem associated_mul_unit_left {N : Type u_3} [Monoid N] (a : N) (u : N) (hu : IsUnit u) :
          Associated (a * u) a
          theorem associated_unit_mul_left {N : Type u_3} [CommMonoid N] (a : N) (u : N) (hu : IsUnit u) :
          Associated (u * a) a
          theorem associated_mul_unit_right {N : Type u_3} [Monoid N] (a : N) (u : N) (hu : IsUnit u) :
          Associated a (a * u)
          theorem associated_unit_mul_right {N : Type u_3} [CommMonoid N] (a : N) (u : N) (hu : IsUnit u) :
          Associated a (u * a)
          theorem associated_mul_isUnit_left_iff {N : Type u_3} [Monoid N] {a : N} {u : N} {b : N} (hu : IsUnit u) :
          theorem associated_isUnit_mul_left_iff {N : Type u_3} [CommMonoid N] {u : N} {a : N} {b : N} (hu : IsUnit u) :
          theorem associated_mul_isUnit_right_iff {N : Type u_3} [Monoid N] {a : N} {b : N} {u : N} (hu : IsUnit u) :
          theorem associated_isUnit_mul_right_iff {N : Type u_3} [CommMonoid N] {a : N} {u : N} {b : N} (hu : IsUnit u) :
          @[simp]
          theorem associated_mul_unit_left_iff {N : Type u_3} [Monoid N] {a : N} {b : N} {u : Nˣ} :
          Associated (a * u) b Associated a b
          @[simp]
          theorem associated_unit_mul_left_iff {N : Type u_3} [CommMonoid N] {a : N} {b : N} {u : Nˣ} :
          Associated (u * a) b Associated a b
          @[simp]
          theorem associated_mul_unit_right_iff {N : Type u_3} [Monoid N] {a : N} {b : N} {u : Nˣ} :
          Associated a (b * u) Associated a b
          @[simp]
          theorem associated_unit_mul_right_iff {N : Type u_3} [CommMonoid N] {a : N} {b : N} {u : Nˣ} :
          Associated a (u * b) Associated a b
          theorem Associated.mul_left {M : Type u_1} [Monoid M] (a : M) {b : M} {c : M} (h : Associated b c) :
          Associated (a * b) (a * c)
          theorem Associated.mul_right {M : Type u_1} [CommMonoid M] {a : M} {b : M} (h : Associated a b) (c : M) :
          Associated (a * c) (b * c)
          theorem Associated.mul_mul {M : Type u_1} [CommMonoid M] {a₁ : M} {a₂ : M} {b₁ : M} {b₂ : M} (h₁ : Associated a₁ b₁) (h₂ : Associated a₂ b₂) :
          Associated (a₁ * a₂) (b₁ * b₂)
          theorem Associated.pow_pow {M : Type u_1} [CommMonoid M] {a : M} {b : M} {n : } (h : Associated a b) :
          Associated (a ^ n) (b ^ n)
          theorem Associated.dvd {M : Type u_1} [Monoid M] {a : M} {b : M} :
          Associated a ba b
          theorem Associated.dvd' {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Associated a b) :
          b a
          theorem Associated.dvd_dvd {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Associated a b) :
          a b b a
          theorem associated_of_dvd_dvd {M : Type u_1} [CancelMonoidWithZero M] {a : M} {b : M} (hab : a b) (hba : b a) :
          theorem dvd_dvd_iff_associated {M : Type u_1} [CancelMonoidWithZero M] {a : M} {b : M} :
          a b b a Associated a b
          instance instDecidableRelAssociatedOfDvd {M : Type u_1} [CancelMonoidWithZero M] [DecidableRel fun (x1 x2 : M) => x1 x2] :
          DecidableRel fun (x1 x2 : M) => Associated x1 x2
          Equations
          theorem Associated.dvd_iff_dvd_left {M : Type u_1} [Monoid M] {a : M} {b : M} {c : M} (h : Associated a b) :
          a c b c
          theorem Associated.dvd_iff_dvd_right {M : Type u_1} [Monoid M] {a : M} {b : M} {c : M} (h : Associated b c) :
          a b a c
          theorem Associated.eq_zero_iff {M : Type u_1} [MonoidWithZero M] {a : M} {b : M} (h : Associated a b) :
          a = 0 b = 0
          theorem Associated.ne_zero_iff {M : Type u_1} [MonoidWithZero M] {a : M} {b : M} (h : Associated a b) :
          a 0 b 0
          theorem Associated.neg_left {M : Type u_1} [Monoid M] [HasDistribNeg M] {a : M} {b : M} (h : Associated a b) :
          theorem Associated.neg_right {M : Type u_1} [Monoid M] [HasDistribNeg M] {a : M} {b : M} (h : Associated a b) :
          theorem Associated.neg_neg {M : Type u_1} [Monoid M] [HasDistribNeg M] {a : M} {b : M} (h : Associated a b) :
          Associated (-a) (-b)
          theorem Associated.prime {M : Type u_1} [CommMonoidWithZero M] {p : M} {q : M} (h : Associated p q) (hp : Prime p) :
          theorem prime_mul_iff {M : Type u_1} [CancelCommMonoidWithZero M] {x : M} {y : M} :
          @[simp]
          theorem prime_pow_iff {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {n : } :
          Prime (p ^ n) Prime p n = 1
          theorem Irreducible.dvd_iff {M : Type u_1} [Monoid M] {x : M} {y : M} (hx : Irreducible x) :
          theorem Irreducible.associated_of_dvd {M : Type u_1} [Monoid M] {p : M} {q : M} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p q) :
          theorem Irreducible.dvd_irreducible_iff_associated {M : Type u_1} [Monoid M] {p : M} {q : M} (pp : Irreducible p) (qp : Irreducible q) :
          theorem Prime.associated_of_dvd {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {q : M} (p_prime : Prime p) (q_prime : Prime q) (dvd : p q) :
          theorem Prime.dvd_prime_iff_associated {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {q : M} (pp : Prime p) (qp : Prime q) :
          theorem Associated.prime_iff {M : Type u_1} [CommMonoidWithZero M] {p : M} {q : M} (h : Associated p q) :
          theorem Associated.isUnit {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Associated a b) :
          IsUnit aIsUnit b
          theorem Associated.isUnit_iff {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Associated a b) :
          theorem Irreducible.isUnit_iff_not_associated_of_dvd {M : Type u_1} [Monoid M] {x : M} {y : M} (hx : Irreducible x) (hy : y x) :
          theorem Associated.irreducible {M : Type u_1} [Monoid M] {p : M} {q : M} (h : Associated p q) (hp : Irreducible p) :
          theorem Associated.irreducible_iff {M : Type u_1} [Monoid M] {p : M} {q : M} (h : Associated p q) :
          theorem Associated.of_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] {a : M} {b : M} {c : M} {d : M} (h : Associated (a * b) (c * d)) (h₁ : Associated a c) (ha : a 0) :
          theorem Associated.of_mul_right {M : Type u_1} [CancelCommMonoidWithZero M] {a : M} {b : M} {c : M} {d : M} :
          Associated (a * b) (c * d)Associated b db 0Associated a c
          theorem Associated.of_pow_associated_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] {p₁ : M} {p₂ : M} {k₁ : } {k₂ : } (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : Associated (p₁ ^ k₁) (p₂ ^ k₂)) :
          Associated p₁ p₂
          theorem Associated.of_pow_associated_of_prime' {M : Type u_1} [CancelCommMonoidWithZero M] {p₁ : M} {p₂ : M} {k₁ : } {k₂ : } (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₂ : 0 < k₂) (h : Associated (p₁ ^ k₁) (p₂ ^ k₂)) :
          Associated p₁ p₂
          theorem Irreducible.isRelPrime_iff_not_dvd {M : Type u_1} [Monoid M] {p : M} {n : M} (hp : Irreducible p) :

          See also Irreducible.coprime_iff_not_dvd.

          theorem Irreducible.dvd_or_isRelPrime {M : Type u_1} [Monoid M] {p : M} {n : M} (hp : Irreducible p) :
          theorem associated_iff_eq {M : Type u_1} [Monoid M] [Subsingleton Mˣ] {x : M} {y : M} :
          Associated x y x = y
          theorem associated_eq_eq {M : Type u_1} [Monoid M] [Subsingleton Mˣ] :
          Associated = Eq
          theorem prime_dvd_prime_iff_eq {M : Type u_3} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p : M} {q : M} (pp : Prime p) (qp : Prime q) :
          p q p = q
          theorem eq_of_prime_pow_eq {R : Type u_3} [CancelCommMonoidWithZero R] [Subsingleton Rˣ] {p₁ : R} {p₂ : R} {k₁ : } {k₂ : } (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :
          p₁ = p₂
          theorem eq_of_prime_pow_eq' {R : Type u_3} [CancelCommMonoidWithZero R] [Subsingleton Rˣ] {p₁ : R} {p₂ : R} {k₁ : } {k₂ : } (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
          p₁ = p₂
          @[reducible, inline]
          abbrev Associates (M : Type u_3) [Monoid M] :
          Type u_3

          The quotient of a monoid by the Associated relation. Two elements x and y are associated iff there is a unit u such that x * u = y. There is a natural monoid structure on Associates M.

          Equations
          Instances For
            @[reducible, inline]
            abbrev Associates.mk {M : Type u_3} [Monoid M] (a : M) :

            The canonical quotient map from a monoid M into the Associates of M

            Equations
            Instances For
              Equations
              • Associates.instInhabited = { default := 1 }
              theorem Associates.quotient_mk_eq_mk {M : Type u_1} [Monoid M] (a : M) :
              a = Associates.mk a
              theorem Associates.quot_mk_eq_mk {M : Type u_1} [Monoid M] (a : M) :
              Quot.mk Setoid.r a = Associates.mk a
              @[simp]
              theorem Associates.quot_out {M : Type u_1} [Monoid M] (a : Associates M) :
              theorem Associates.forall_associated {M : Type u_1} [Monoid M] {p : Associates MProp} :
              (∀ (a : Associates M), p a) ∀ (a : M), p (Associates.mk a)
              theorem Associates.mk_surjective {M : Type u_1} [Monoid M] :
              Function.Surjective Associates.mk
              instance Associates.instOne {M : Type u_1} [Monoid M] :
              Equations
              • Associates.instOne = { one := 1 }
              @[simp]
              theorem Associates.mk_one {M : Type u_1} [Monoid M] :
              @[simp]
              theorem Associates.mk_eq_one {M : Type u_1} [Monoid M] {a : M} :
              instance Associates.instBot {M : Type u_1} [Monoid M] :
              Equations
              • Associates.instBot = { bot := 1 }
              theorem Associates.bot_eq_one {M : Type u_1} [Monoid M] :
              = 1
              theorem Associates.exists_rep {M : Type u_1} [Monoid M] (a : Associates M) :
              ∃ (a0 : M), Associates.mk a0 = a
              Equations
              • Associates.instUniqueOfSubsingleton = { default := 1, uniq := }
              instance Associates.instMul {M : Type u_1} [CommMonoid M] :
              Equations
              theorem Associates.mk_mul_mk {M : Type u_1} [CommMonoid M] {x : M} {y : M} :
              Equations
              Equations

              Associates.mk as a MonoidHom.

              Equations
              • Associates.mkMonoidHom = { toFun := Associates.mk, map_one' := , map_mul' := }
              Instances For
                @[simp]
                theorem Associates.mkMonoidHom_apply {M : Type u_1} [CommMonoid M] (a : M) :
                Associates.mkMonoidHom a = Associates.mk a
                theorem Associates.associated_map_mk {M : Type u_1} [CommMonoid M] {f : Associates M →* M} (hinv : Function.RightInverse (⇑f) Associates.mk) (a : M) :
                theorem Associates.mk_pow {M : Type u_1} [CommMonoid M] (a : M) (n : ) :
                theorem Associates.dvd_eq_le {M : Type u_1} [CommMonoid M] :
                (fun (x1 x2 : Associates M) => x1 x2) = fun (x1 x2 : Associates M) => x1 x2
                Equations
                • Associates.uniqueUnits = { toInhabited := Units.instInhabited, uniq := }
                @[deprecated mul_eq_one]
                theorem Associates.mul_eq_one_iff {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} :
                a * b = 1 a = 1 b = 1

                Alias of mul_eq_one.

                @[deprecated Subsingleton.elim]
                theorem Associates.units_eq_one {α : Sort u} [h : Subsingleton α] (a : α) (b : α) :
                a = b

                Alias of Subsingleton.elim.

                @[simp]
                theorem Associates.coe_unit_eq_one {M : Type u_1} [CommMonoid M] (u : (Associates M)ˣ) :
                u = 1
                theorem Associates.mul_mono {M : Type u_1} [CommMonoid M] {a : Associates M} {b : Associates M} {c : Associates M} {d : Associates M} (h₁ : a b) (h₂ : c d) :
                a * c b * d
                theorem Associates.one_le {M : Type u_1} [CommMonoid M] {a : Associates M} :
                1 a
                theorem Associates.le_mul_right {M : Type u_1} [CommMonoid M] {a : Associates M} {b : Associates M} :
                a a * b
                theorem Associates.le_mul_left {M : Type u_1} [CommMonoid M] {a : Associates M} {b : Associates M} :
                a b * a
                Equations
                @[simp]
                theorem Associates.mk_dvd_mk {M : Type u_1} [CommMonoid M] {a : M} {b : M} :
                theorem Associates.dvd_of_mk_le_mk {M : Type u_1} [CommMonoid M] {a : M} {b : M} :
                theorem Associates.mk_le_mk_of_dvd {M : Type u_1} [CommMonoid M] {a : M} {b : M} :
                @[deprecated Associates.mk_le_mk_iff_dvd]
                theorem Associates.mk_le_mk_iff_dvd_iff {M : Type u_1} [CommMonoid M] {a : M} {b : M} :

                Alias of Associates.mk_le_mk_iff_dvd.

                @[simp]
                @[deprecated Associates.isPrimal_mk]

                Alias of Associates.isPrimal_mk.

                @[simp]
                instance Associates.instZero {M : Type u_1} [Zero M] [Monoid M] :
                Equations
                • Associates.instZero = { zero := 0 }
                instance Associates.instTopOfZero {M : Type u_1} [Zero M] [Monoid M] :
                Equations
                • Associates.instTopOfZero = { top := 0 }
                @[simp]
                theorem Associates.mk_zero {M : Type u_1} [Zero M] [Monoid M] :
                @[simp]
                theorem Associates.mk_eq_zero {M : Type u_1} [MonoidWithZero M] {a : M} :
                @[simp]
                theorem Associates.mk_ne_zero {M : Type u_1} [MonoidWithZero M] {a : M} :
                Equations
                • =
                theorem Associates.exists_non_zero_rep {M : Type u_1} [MonoidWithZero M] {a : Associates M} :
                a 0∃ (a0 : M), a0 0 Associates.mk a0 = a
                Equations
                Equations
                @[simp]
                theorem Associates.le_zero {M : Type u_1} [CommMonoidWithZero M] (a : Associates M) :
                a 0
                Equations
                • Associates.instBoundedOrder = BoundedOrder.mk
                instance Associates.instDecidableRelDvd {M : Type u_1} [CommMonoidWithZero M] [DecidableRel fun (x1 x2 : M) => x1 x2] :
                DecidableRel fun (x1 x2 : Associates M) => x1 x2
                Equations
                theorem Associates.Prime.le_or_le {M : Type u_1} [CommMonoidWithZero M] {p : Associates M} (hp : Prime p) {a : Associates M} {b : Associates M} (h : p a * b) :
                p a p b
                @[simp]
                theorem Associates.dvdNotUnit_of_lt {M : Type u_1} [CommMonoidWithZero M] {a : Associates M} {b : Associates M} (hlt : a < b) :
                Equations
                Equations
                • Associates.instCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk
                theorem Associates.le_of_mul_le_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] (a : Associates M) (b : Associates M) (c : Associates M) (ha : a 0) :
                a * b a * cb c
                theorem Associates.one_or_eq_of_le_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] {p : Associates M} {m : Associates M} (hp : Prime p) (hle : m p) :
                m = 1 m = p
                theorem DvdNotUnit.isUnit_of_irreducible_right {M : Type u_1} [CommMonoidWithZero M] {p : M} {q : M} (h : DvdNotUnit p q) (hq : Irreducible q) :
                theorem not_irreducible_of_not_unit_dvdNotUnit {M : Type u_1} [CommMonoidWithZero M] {p : M} {q : M} (hp : ¬IsUnit p) (h : DvdNotUnit p q) :
                theorem DvdNotUnit.not_unit {M : Type u_1} [CommMonoidWithZero M] {p : M} {q : M} (hp : DvdNotUnit p q) :
                theorem dvdNotUnit_of_dvdNotUnit_associated {M : Type u_1} [CommMonoidWithZero M] [Nontrivial M] {p : M} {q : M} {r : M} (h : DvdNotUnit p q) (h' : Associated q r) :
                theorem isUnit_of_associated_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {b : M} (h : Associated (p * b) p) (hp : p 0) :
                theorem DvdNotUnit.not_associated {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {q : M} (h : DvdNotUnit p q) :
                theorem DvdNotUnit.ne {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {q : M} (h : DvdNotUnit p q) :
                p q
                theorem pow_injective_of_not_isUnit {M : Type u_1} [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q 0) :
                Function.Injective fun (n : ) => q ^ n
                @[deprecated pow_injective_of_not_isUnit]
                theorem pow_injective_of_not_unit {M : Type u_1} [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q 0) :
                Function.Injective fun (n : ) => q ^ n

                Alias of pow_injective_of_not_isUnit.

                theorem pow_inj_of_not_isUnit {M : Type u_1} [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q 0) {m : } {n : } :
                q ^ m = q ^ n m = n
                theorem dvd_prime_pow {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {q : M} (hp : Prime p) (n : ) :
                q p ^ n ∃ (i : ), i n Associated q (p ^ i)