# 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.

source
def Associated {M : Type u_1} [Monoid M] (x y : M) :
Prop

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

Equations

- Associated x y = ∃ (u : M ˣ), x * ↑u = y

Instances For

source
theorem Associated.refl {M : Type u_1} [Monoid M] (x : M) :
Associated x x
source
theorem Associated.rfl {M : Type u_1} [Monoid M] {x : M} :
Associated x x
source
instance Associated.instIsRefl {M : Type u_1} [Monoid M] :
IsRefl M Associated
source
theorem Associated.symm {M : Type u_1} [Monoid M] {x y : M} :
Associated x y → Associated y x
source
instance Associated.instIsSymm {M : Type u_1} [Monoid M] :
IsSymm M Associated
source
theorem Associated.comm {M : Type u_1} [Monoid M] {x y : M} :
Associated x y ↔ Associated y x
source
theorem Associated.trans {M : Type u_1} [Monoid M] {x y z : M} :
Associated x y → Associated y z → Associated x z
source
instance Associated.instIsTrans {M : Type u_1} [Monoid M] :
IsTrans M Associated
source
def Associated.setoid (M : Type u_2) [Monoid M] :
Setoid M

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

Equations

- Associated.setoid M = { r := Associated, iseqv := ⋯ }

Instances For

source
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)
source
theorem Associated.of_eq {M : Type u_1} [Monoid M] {a b : M} (h : a = b) :
Associated a b
source
theorem unit_associated_one {M : Type u_1} [Monoid M] {u : M ˣ} :
Associated (↑u) 1
source
@[simp]
theorem associated_one_iff_isUnit {M : Type u_1} [Monoid M] {a : M} :
Associated a 1 ↔ IsUnit a
source
@[simp]
theorem associated_zero_iff_eq_zero {M : Type u_1} [MonoidWithZero M] (a : M) :
Associated a 0 ↔ a = 0
source
theorem associated_one_of_mul_eq_one {M : Type u_1} [CommMonoid M] {a : M} (b : M) (hab : a * b = 1) :
Associated a 1
source
theorem associated_one_of_associated_mul_one {M : Type u_1} [CommMonoid M] {a b : M} :
Associated (a * b) 1 → Associated a 1
source
theorem associated_mul_unit_left {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :
Associated (a * u) a
source
theorem associated_unit_mul_left {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :
Associated (u * a) a
source
theorem associated_mul_unit_right {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :
Associated a (a * u)
source
theorem associated_unit_mul_right {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :
Associated a (u * a)
source
theorem associated_mul_isUnit_left_iff {N : Type u_2} [Monoid N] {a u b : N} (hu : IsUnit u) :
Associated (a * u) b ↔ Associated a b
source
theorem associated_isUnit_mul_left_iff {N : Type u_2} [CommMonoid N] {u a b : N} (hu : IsUnit u) :
Associated (u * a) b ↔ Associated a b
source
theorem associated_mul_isUnit_right_iff {N : Type u_2} [Monoid N] {a b u : N} (hu : IsUnit u) :
Associated a (b * u) ↔ Associated a b
source
theorem associated_isUnit_mul_right_iff {N : Type u_2} [CommMonoid N] {a u b : N} (hu : IsUnit u) :
Associated a (u * b) ↔ Associated a b
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem Associated.mul_left {M : Type u_1} [Monoid M] (a : M) {b c : M} (h : Associated b c) :
Associated (a * b) (a * c)
source
theorem Associated.mul_right {M : Type u_1} [CommMonoid M] {a b : M} (h : Associated a b) (c : M) :
Associated (a * c) (b * c)
source
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₂)
source
theorem Associated.pow_pow {M : Type u_1} [CommMonoid M] {a b : M} {n : ℕ} (h : Associated a b) :
Associated (a ^ n) (b ^ n)
source
theorem Associated.dvd {M : Type u_1} [Monoid M] {a b : M} :
Associated a b → a ∣ b
source
theorem Associated.dvd' {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
b ∣ a
source
theorem Associated.dvd_dvd {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
a ∣ b ∧ b ∣ a
source
theorem associated_of_dvd_dvd {M : Type u_1} [CancelMonoidWithZero M] {a b : M} (hab : a ∣ b) (hba : b ∣ a) :
Associated a b
source
theorem dvd_dvd_iff_associated {M : Type u_1} [CancelMonoidWithZero M] {a b : M} :
a ∣ b ∧ b ∣ a ↔ Associated a b
source
instance instDecidableRelAssociatedOfDvd {M : Type u_1} [CancelMonoidWithZero M] [DecidableRel fun (x1 x2 : M) => x1 ∣ x2] :
DecidableRel fun (x1 x2 : M) => Associated x1 x2
Equations

- instDecidableRelAssociatedOfDvd x✝¹ x✝ = decidable_of_iff (x✝¹ ∣ x✝ ∧ x✝ ∣ x✝¹) ⋯

source
theorem Associated.dvd_iff_dvd_left {M : Type u_1} [Monoid M] {a b c : M} (h : Associated a b) :
a ∣ c ↔ b ∣ c
source
theorem Associated.dvd_iff_dvd_right {M : Type u_1} [Monoid M] {a b c : M} (h : Associated b c) :
a ∣ b ↔ a ∣ c
source
theorem Associated.eq_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :
a = 0 ↔ b = 0
source
theorem Associated.ne_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :
a ≠ 0 ↔ b ≠ 0
source
theorem Associated.prime {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) (hp : Prime p) :
Prime q
source
theorem prime_mul_iff {M : Type u_1} [CancelCommMonoidWithZero M] {x y : M} :
Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
source
@[simp]
theorem prime_pow_iff {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {n : ℕ} :
Prime (p ^ n) ↔ Prime p ∧ n = 1
source
theorem Irreducible.dvd_iff {M : Type u_1} [Monoid M] {x y : M} (hx : Irreducible x) :
y ∣ x ↔ IsUnit y ∨ Associated x y
source
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) :
Associated p q
source
theorem Irreducible.dvd_irreducible_iff_associated {M : Type u_1} [Monoid M] {p q : M} (pp : Irreducible p) (qp : Irreducible q) :
p ∣ q ↔ Associated p q
source
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) :
Associated p q
source
theorem Prime.dvd_prime_iff_associated {M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (pp : Prime p) (qp : Prime q) :
p ∣ q ↔ Associated p q
source
theorem Associated.prime_iff {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) :
Prime p ↔ Prime q
source
theorem Associated.isUnit {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
IsUnit a → IsUnit b
source
theorem Associated.isUnit_iff {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :
IsUnit a ↔ IsUnit b
source
theorem Irreducible.isUnit_iff_not_associated_of_dvd {M : Type u_1} [Monoid M] {x y : M} (hx : Irreducible x) (hy : y ∣ x) :
IsUnit y ↔ ¬Associated x y
source
theorem Associated.irreducible {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) (hp : Irreducible p) :
Irreducible q
source
theorem Associated.irreducible_iff {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) :
Irreducible p ↔ Irreducible q
source
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) :
Associated b d
source
theorem Associated.of_mul_right {M : Type u_1} [CancelCommMonoidWithZero M] {a b c d : M} :
Associated (a * b) (c * d) → Associated b d → b ≠ 0 → Associated a c
source
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₂
source
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₂
source
theorem Irreducible.isRelPrime_iff_not_dvd {M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) :
IsRelPrime p n ↔ ¬p ∣ n

See also `Irreducible.coprime_iff_not_dvd`.

source
theorem Irreducible.dvd_or_isRelPrime {M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) :
p ∣ n ∨ IsRelPrime p n
source
theorem associated_iff_eq {M : Type u_1} [Monoid M] [Subsingleton M ˣ] {x y : M} :
Associated x y ↔ x = y
source
theorem associated_eq_eq {M : Type u_1} [Monoid M] [Subsingleton M ˣ] :
Associated = Eq
source
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
source
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₂
source
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₂
source
@[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

- Associates M = Quotient (Associated.setoid M)

Instances For

source
@[reducible, inline]
abbrev Associates.mk {M : Type u_2} [Monoid M] (a : M) :
Associates M

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

Equations

- Associates.mk a = ⟦a⟧

Instances For

source
instance Associates.instInhabited {M : Type u_1} [Monoid M] :
Inhabited (Associates M)
Equations

- Associates.instInhabited = { default := ⟦1⟧ }

source
theorem Associates.mk_eq_mk_iff_associated {M : Type u_1} [Monoid M] {a b : M} :
Associates.mk a = Associates.mk b ↔ Associated a b
source
theorem Associates.quotient_mk_eq_mk {M : Type u_1} [Monoid M] (a : M) :
⟦a⟧ = Associates.mk a
source
theorem Associates.quot_mk_eq_mk {M : Type u_1} [Monoid M] (a : M) :
Quot.mk (⇑(Associated.setoid M)) a = Associates.mk a
source
@[simp]
theorem Associates.quot_out {M : Type u_1} [Monoid M] (a : Associates M) :
Associates.mk (Quot.out a) = a
source
theorem Associates.mk_quot_out {M : Type u_1} [Monoid M] (a : M) :
Associated (Quot.out (Associates.mk a)) a
source
theorem Associates.forall_associated {M : Type u_1} [Monoid M] {p : Associates M → Prop} :
(∀ (a : Associates M), p a) ↔ ∀ (a : M), p (Associates.mk a)
source
theorem Associates.mk_surjective {M : Type u_1} [Monoid M] :
Function.Surjective Associates.mk
source
instance Associates.instOne {M : Type u_1} [Monoid M] :
One (Associates M)
Equations

- Associates.instOne = { one := ⟦1⟧ }

source
@[simp]
theorem Associates.mk_one {M : Type u_1} [Monoid M] :
Associates.mk 1 = 1
source
theorem Associates.one_eq_mk_one {M : Type u_1} [Monoid M] :
1 = Associates.mk 1
source
@[simp]
theorem Associates.mk_eq_one {M : Type u_1} [Monoid M] {a : M} :
Associates.mk a = 1 ↔ IsUnit a
source
instance Associates.instBot {M : Type u_1} [Monoid M] :
Bot (Associates M)
Equations

- Associates.instBot = { bot := 1 }

source
theorem Associates.bot_eq_one {M : Type u_1} [Monoid M] :
⊥ = 1
source
theorem Associates.exists_rep {M : Type u_1} [Monoid M] (a : Associates M) :
∃ (a0 : M), Associates.mk a0 = a
source
instance Associates.instUniqueOfSubsingleton {M : Type u_1} [Monoid M] [Subsingleton M] :
Unique (Associates M)
Equations

- Associates.instUniqueOfSubsingleton = { default := 1, uniq := ⋯ }

source
theorem Associates.mk_injective {M : Type u_1} [Monoid M] [Subsingleton M ˣ] :
Function.Injective Associates.mk
source
instance Associates.instMul {M : Type u_1} [CommMonoid M] :
Mul (Associates M)
Equations

- Associates.instMul = { mul := Quotient.map₂ (fun (x1 x2 : M) => x1 * x2) ⋯ }

source
theorem Associates.mk_mul_mk {M : Type u_1} [CommMonoid M] {x y : M} :
Associates.mk x * Associates.mk y = Associates.mk (x * y)
source
instance Associates.instCommMonoid {M : Type u_1} [CommMonoid M] :
CommMonoid (Associates M)
Equations

- One or more equations did not get rendered due to their size.

source
instance Associates.instPreorder {M : Type u_1} [CommMonoid M] :
Preorder (Associates M)
Equations

- Associates.instPreorder = { le := Dvd.dvd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

source
def Associates.mkMonoidHom {M : Type u_1} [CommMonoid M] :
M →* Associates M

`Associates.mk` as a `MonoidHom`.

Equations

- Associates.mkMonoidHom = { toFun := Associates.mk, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Associates.mkMonoidHom_apply {M : Type u_1} [CommMonoid M] (a : M) :
Associates.mkMonoidHom a = Associates.mk a
source
theorem Associates.associated_map_mk {M : Type u_1} [CommMonoid M] {f : Associates M →* M} (hinv : Function.RightInverse (⇑f) Associates.mk) (a : M) :
Associated a (f (Associates.mk a))
source
theorem Associates.mk_pow {M : Type u_1} [CommMonoid M] (a : M) (n : ℕ) :
Associates.mk (a ^ n) = Associates.mk a ^ n
source
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
source
instance Associates.uniqueUnits {M : Type u_1} [CommMonoid M] :
Unique (Associates M)ˣ
Equations

- Associates.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

source
@[simp]
theorem Associates.coe_unit_eq_one {M : Type u_1} [CommMonoid M] (u : (Associates M)ˣ) :
↑u = 1
source
theorem Associates.isUnit_iff_eq_one {M : Type u_1} [CommMonoid M] (a : Associates M) :
IsUnit a ↔ a = 1
source
theorem Associates.isUnit_iff_eq_bot {M : Type u_1} [CommMonoid M] {a : Associates M} :
IsUnit a ↔ a = ⊥
source
theorem Associates.isUnit_mk {M : Type u_1} [CommMonoid M] {a : M} :
IsUnit (Associates.mk a) ↔ IsUnit a
source
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
source
theorem Associates.one_le {M : Type u_1} [CommMonoid M] {a : Associates M} :
1 ≤ a
source
theorem Associates.le_mul_right {M : Type u_1} [CommMonoid M] {a b : Associates M} :
a ≤ a * b
source
theorem Associates.le_mul_left {M : Type u_1} [CommMonoid M] {a b : Associates M} :
a ≤ b * a
source
instance Associates.instOrderBot {M : Type u_1} [CommMonoid M] :
OrderBot (Associates M)
Equations

- Associates.instOrderBot = { bot := 1, bot_le := ⋯ }

source
@[simp]
theorem Associates.mk_dvd_mk {M : Type u_1} [CommMonoid M] {a b : M} :
Associates.mk a ∣ Associates.mk b ↔ a ∣ b
source
theorem Associates.dvd_of_mk_le_mk {M : Type u_1} [CommMonoid M] {a b : M} :
Associates.mk a ≤ Associates.mk b → a ∣ b
source
theorem Associates.mk_le_mk_of_dvd {M : Type u_1} [CommMonoid M] {a b : M} :
a ∣ b → Associates.mk a ≤ Associates.mk b
source
theorem Associates.mk_le_mk_iff_dvd {M : Type u_1} [CommMonoid M] {a b : M} :
Associates.mk a ≤ Associates.mk b ↔ a ∣ b
source
@[simp]
theorem Associates.isPrimal_mk {M : Type u_1} [CommMonoid M] {a : M} :
IsPrimal (Associates.mk a) ↔ IsPrimal a
source
@[simp]
theorem Associates.decompositionMonoid_iff {M : Type u_1} [CommMonoid M] :
DecompositionMonoid (Associates M) ↔ DecompositionMonoid M
source
instance Associates.instDecompositionMonoid {M : Type u_1} [CommMonoid M] [DecompositionMonoid M] :
DecompositionMonoid (Associates M)
source
@[simp]
theorem Associates.mk_isRelPrime_iff {M : Type u_1} [CommMonoid M] {a b : M} :
IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
source
instance Associates.instZero {M : Type u_1} [Zero M] [Monoid M] :
Zero (Associates M)
Equations

- Associates.instZero = { zero := ⟦0⟧ }

source
instance Associates.instTopOfZero {M : Type u_1} [Zero M] [Monoid M] :
Top (Associates M)
Equations

- Associates.instTopOfZero = { top := 0 }

source
@[simp]
theorem Associates.mk_zero {M : Type u_1} [Zero M] [Monoid M] :
Associates.mk 0 = 0
source
@[simp]
theorem Associates.mk_eq_zero {M : Type u_1} [MonoidWithZero M] {a : M} :
Associates.mk a = 0 ↔ a = 0
source
@[simp]
theorem Associates.quot_out_zero {M : Type u_1} [MonoidWithZero M] :
Quot.out 0 = 0
source
theorem Associates.mk_ne_zero {M : Type u_1} [MonoidWithZero M] {a : M} :
Associates.mk a ≠ 0 ↔ a ≠ 0
source
instance Associates.instNontrivial {M : Type u_1} [MonoidWithZero M] [Nontrivial M] :
Nontrivial (Associates M)
source
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
source
instance Associates.instCommMonoidWithZero {M : Type u_1} [CommMonoidWithZero M] :
CommMonoidWithZero (Associates M)
Equations

- Associates.instCommMonoidWithZero = { toCommMonoid := Associates.instCommMonoid, toZero := Associates.instZero, zero_mul := ⋯, mul_zero := ⋯ }

source
instance Associates.instOrderTop {M : Type u_1} [CommMonoidWithZero M] :
OrderTop (Associates M)
Equations

- Associates.instOrderTop = { top := 0, le_top := ⋯ }

source
@[simp]
theorem Associates.le_zero {M : Type u_1} [CommMonoidWithZero M] (a : Associates M) :
a ≤ 0
source
instance Associates.instBoundedOrder {M : Type u_1} [CommMonoidWithZero M] :
BoundedOrder (Associates M)
Equations

- Associates.instBoundedOrder = { toOrderTop := Associates.instOrderTop, toOrderBot := Associates.instOrderBot }

source
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

- a.instDecidableRelDvd b = Quotient.recOnSubsingleton₂ a b fun (x x_1 : M) => decidable_of_iff' (x ∣ x_1) ⋯

source
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
source
@[simp]
theorem Associates.prime_mk {M : Type u_1} [CommMonoidWithZero M] {p : M} :
Prime (Associates.mk p) ↔ Prime p
source
@[simp]
theorem Associates.irreducible_mk {M : Type u_1} [CommMonoidWithZero M] {a : M} :
Irreducible (Associates.mk a) ↔ Irreducible a
source
@[simp]
theorem Associates.mk_dvdNotUnit_mk_iff {M : Type u_1} [CommMonoidWithZero M] {a b : M} :
DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
source
theorem Associates.dvdNotUnit_of_lt {M : Type u_1} [CommMonoidWithZero M] {a b : Associates M} (hlt : a < b) :
DvdNotUnit a b
source
theorem Associates.irreducible_iff_prime_iff {M : Type u_1} [CommMonoidWithZero M] :
(∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
source
instance Associates.instPartialOrder {M : Type u_1} [CancelCommMonoidWithZero M] :
PartialOrder (Associates M)
Equations

- Associates.instPartialOrder = { toPreorder := Associates.instPreorder, le_antisymm := ⋯ }

source
instance Associates.instCancelCommMonoidWithZero {M : Type u_1} [CancelCommMonoidWithZero M] :
CancelCommMonoidWithZero (Associates M)
Equations

- Associates.instCancelCommMonoidWithZero = { toCommMonoidWithZero := inferInstance, toIsLeftCancelMulZero := ⋯ }

source
theorem associates_irreducible_iff_prime {M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {p : Associates M} :
Irreducible p ↔ Prime p
source
instance Associates.instNoZeroDivisors {M : Type u_1} [CancelCommMonoidWithZero M] :
NoZeroDivisors (Associates M)
source
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 * c → b ≤ c
source
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
source
theorem Associates.dvdNotUnit_iff_lt {M : Type u_1} [CancelCommMonoidWithZero M] {a b : Associates M} :
DvdNotUnit a b ↔ a < b
source
theorem Associates.le_one_iff {M : Type u_1} [CancelCommMonoidWithZero M] {p : Associates M} :
p ≤ 1 ↔ p = 1
source
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) :
DvdNotUnit p r
source
theorem isUnit_of_associated_mul {M : Type u_1} [CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p) (hp : p ≠ 0) :
IsUnit b
source
theorem DvdNotUnit.not_associated {M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) :
¬Associated p q
source
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)