Documentation

Mathlib.Algebra.GroupWithZero.Associated

Associated elements. #

In this file we 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 Associated {M : Type u_1} [Monoid M] (x 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} :
      theorem Associated.symm {M : Type u_1} [Monoid M] {x y : M} :
      theorem Associated.comm {M : Type u_1} [Monoid M] {x y : M} :
      theorem Associated.trans {M : Type u_1} [Monoid M] {x y z : M} :
      Associated x yAssociated y zAssociated x z
      def Associated.setoid (M : Type u_2) [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_2} {N : Type u_3} [Monoid M] [Monoid N] {F : Type u_4} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x 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 b : M} :
          Associated (a * b) 1Associated a 1
          theorem associated_mul_unit_left {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :
          Associated (a * u) a
          theorem associated_unit_mul_left {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :
          Associated (u * a) a
          theorem associated_mul_unit_right {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :
          Associated a (a * u)
          theorem associated_unit_mul_right {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :
          Associated a (u * a)
          theorem associated_mul_isUnit_left_iff {N : Type u_2} [Monoid N] {a u b : N} (hu : IsUnit u) :
          theorem associated_isUnit_mul_left_iff {N : Type u_2} [CommMonoid N] {u a b : N} (hu : IsUnit u) :
          theorem associated_mul_isUnit_right_iff {N : Type u_2} [Monoid N] {a b u : N} (hu : IsUnit u) :
          theorem associated_isUnit_mul_right_iff {N : Type u_2} [CommMonoid N] {a u b : N} (hu : IsUnit u) :
          @[simp]
          theorem associated_mul_unit_left_iff {N : Type u_2} [Monoid N] {a b : N} {u : Nˣ} :
          Associated (a * u) b Associated a b
          @[simp]
          theorem associated_unit_mul_left_iff {N : Type u_2} [CommMonoid N] {a b : N} {u : Nˣ} :
          Associated (u * a) b Associated a b
          @[simp]
          theorem associated_mul_unit_right_iff {N : Type u_2} [Monoid N] {a b : N} {u : Nˣ} :
          Associated a (b * u) Associated a b
          @[simp]
          theorem associated_unit_mul_right_iff {N : Type u_2} [CommMonoid N] {a b : N} {u : Nˣ} :
          Associated a (u * b) Associated a b
          theorem Associated.mul_left {M : Type u_1} [Monoid M] (a : M) {b c : M} (h : Associated b c) :
          Associated (a * b) (a * c)
          theorem Associated.mul_right {M : Type u_1} [CommMonoid M] {a b : M} (h : Associated a b) (c : M) :
          Associated (a * c) (b * c)
          theorem Associated.mul_mul {M : Type u_1} [CommMonoid M] {a₁ a₂ b₁ 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 b : M} {n : } (h : Associated a b) :
          Associated (a ^ n) (b ^ n)
          theorem Associated.dvd {M : Type u_1} [Monoid M] {a b : M} :
          Associated a ba b
          theorem Associated.dvd' {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
          b a
          theorem Associated.dvd_dvd {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
          a b b a
          theorem associated_of_dvd_dvd {M : Type u_1} [CancelMonoidWithZero M] {a b : M} (hab : a b) (hba : b a) :
          theorem dvd_dvd_iff_associated {M : Type u_1} [CancelMonoidWithZero M] {a 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 b c : M} (h : Associated a b) :
            a c b c
            theorem Associated.dvd_iff_dvd_right {M : Type u_1} [Monoid M] {a b c : M} (h : Associated b c) :
            a b a c
            theorem Associated.eq_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :
            a = 0 b = 0
            theorem Associated.ne_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :
            a 0 b 0
            theorem Associated.prime {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) (hp : Prime p) :
            theorem prime_mul_iff {M : Type u_1} [CancelCommMonoidWithZero M] {x 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 y : M} (hx : Irreducible x) :
            theorem Irreducible.associated_of_dvd {M : Type u_1} [Monoid M] {p 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 q : M} (pp : Irreducible p) (qp : Irreducible q) :
            theorem Prime.associated_of_dvd {M : Type u_1} [CancelCommMonoidWithZero M] {p 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 q : M} (pp : Prime p) (qp : Prime q) :
            theorem Associated.prime_iff {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) :
            theorem Associated.isUnit {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
            IsUnit aIsUnit b
            theorem Associated.isUnit_iff {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
            theorem Irreducible.isUnit_iff_not_associated_of_dvd {M : Type u_1} [Monoid M] {x y : M} (hx : Irreducible x) (hy : y x) :
            theorem Associated.irreducible {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) (hp : Irreducible p) :
            theorem Associated.irreducible_iff {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) :
            theorem Associated.of_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] {a b c 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 b c 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₁ 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₁ 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 n : M} (hp : Irreducible p) :

            See also Irreducible.coprime_iff_not_dvd.

            theorem Irreducible.dvd_or_isRelPrime {M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) :
            theorem associated_iff_eq {M : Type u_1} [Monoid M] [Subsingleton Mˣ] {x y : M} :
            Associated x y x = y
            theorem prime_dvd_prime_iff_eq {M : Type u_2} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M} (pp : Prime p) (qp : Prime q) :
            p q p = q
            theorem eq_of_prime_pow_eq {R : Type u_2} [CancelCommMonoidWithZero R] [Subsingleton Rˣ] {p₁ 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_2} [CancelCommMonoidWithZero R] [Subsingleton Rˣ] {p₁ 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_2) [Monoid M] :
            Type u_2

            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_2} [Monoid M] (a : M) :

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

                Equations
                  Instances For
                    Equations
                      @[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)
                      instance Associates.instOne {M : Type u_1} [Monoid M] :
                      Equations
                        @[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
                          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) :
                          instance Associates.instMul {M : Type u_1} [CommMonoid M] :
                          Equations
                            Equations

                              Associates.mk as a MonoidHom.

                              Equations
                                Instances For
                                  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
                                    @[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 b c 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 b : Associates M} :
                                    a a * b
                                    theorem Associates.le_mul_left {M : Type u_1} [CommMonoid M] {a b : Associates M} :
                                    a b * a
                                    Equations
                                      @[simp]
                                      theorem Associates.mk_dvd_mk {M : Type u_1} [CommMonoid M] {a b : M} :
                                      @[simp]
                                      instance Associates.instZero {M : Type u_1} [Zero M] [Monoid M] :
                                      Equations
                                        instance Associates.instTopOfZero {M : Type u_1} [Zero M] [Monoid M] :
                                        Equations
                                          @[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} :
                                          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
                                          @[simp]
                                          theorem Associates.le_zero {M : Type u_1} [CommMonoidWithZero M] (a : Associates M) :
                                          a 0
                                          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 b : Associates M} (h : p a * b) :
                                            p a p b
                                            @[simp]
                                            theorem Associates.dvdNotUnit_of_lt {M : Type u_1} [CommMonoidWithZero M] {a b : Associates M} (hlt : a < b) :
                                            theorem Associates.le_of_mul_le_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] (a b 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 m : Associates M} (hp : Prime p) (hle : m p) :
                                            m = 1 m = p
                                            theorem dvdNotUnit_of_dvdNotUnit_associated {M : Type u_1} [CommMonoidWithZero M] [Nontrivial M] {p q r : M} (h : DvdNotUnit p q) (h' : Associated q r) :
                                            theorem isUnit_of_associated_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p) (hp : p 0) :
                                            theorem dvd_prime_pow {M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (hp : Prime p) (n : ) :
                                            q p ^ n (i : ), i n Associated q (p ^ i)