Order on associates of a monoid with zero

This file shows that the divisibility preorder on Associates M is a partial order when M is cancellative that it has 0 as a top element.

@[instance_reducible]

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

Equations

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

@[simp]

theorem Associates.le_zero {M : Type u_1} [CommMonoidWithZero M] (a : Associates M) : a ≤ 0

theorem Associates.Prime.le_or_le {M : Type u_1} [CommMonoidWithZero M] {p a b : Associates M} (hp : Prime p) (h : p ≤ a * b) : p ≤ a ∨ p ≤ b

theorem Associates.dvdNotUnit_of_lt {M : Type u_1} [CommMonoidWithZero M] {a b : Associates M} (hlt : a < b) : DvdNotUnit a b

@[instance_reducible]

instance Associates.instBoundedOrder {M : Type u_1} [CommMonoidWithZero M] : BoundedOrder (Associates M)

Equations

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

instance Associates.instIsOrderedMonoid {M : Type u_1} [CommMonoidWithZero M] : IsOrderedMonoid (Associates M)

instance Associates.instCanonicallyOrderedMul {M : Type u_1} [CommMonoidWithZero M] : CanonicallyOrderedMul (Associates M)

@[instance_reducible]

instance Associates.instPartialOrder {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] : PartialOrder (Associates M)

Equations

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

theorem Associates.le_of_mul_le_mul_left {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] (a b c : Associates M) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c

theorem Associates.one_or_eq_of_le_of_prime {M : Type u_1} [CommMonoidWithZero M] {p a : Associates M} [IsCancelMulZero M] (hp : Prime p) (hap : a ≤ p) : a = 1 ∨ a = p

theorem Associates.dvdNotUnit_iff_lt {M : Type u_1} [CommMonoidWithZero M] {a b : Associates M} [IsCancelMulZero M] : DvdNotUnit a b ↔ a < b

theorem Associates.le_one_iff {M : Type u_1} [CommMonoidWithZero M] {p : Associates M} [IsCancelMulZero M] : p ≤ 1 ↔ p = 1