Order on associates of a monoid

This file puts the divisibility preorder on Associates M and shows that it has 1 as a bottom element.

@[instance_reducible]

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 := ⋯ }

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

theorem Associates.isUnit_iff_eq_bot {M : Type u_1} [CommMonoid M] {a : Associates M} : IsUnit a ↔ a = ⊥

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

instance Associates.instIsBotOneClass {M : Type u_1} [CommMonoid M] : IsBotOneClass (Associates M)

@[instance_reducible]

instance Associates.instOrderBot {M : Type u_1} [CommMonoid M] : OrderBot (Associates M)

Equations

• Associates.instOrderBot = { toBot := Associates.instBot, bot_le := ⋯ }

@[deprecated one_le (since := "2026-05-07")]

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

theorem Associates.dvd_of_mk_le_mk {M : Type u_1} [CommMonoid M] {x y : M} : Associates.mk x ≤ Associates.mk y → x ∣ y

theorem Associates.mk_le_mk_of_dvd {M : Type u_1} [CommMonoid M] {x y : M} : x ∣ y → Associates.mk x ≤ Associates.mk y

theorem Associates.mk_le_mk_iff_dvd {M : Type u_1} [CommMonoid M] {x y : M} : Associates.mk x ≤ Associates.mk y ↔ x ∣ y