# mathlibdocumentation

algebra.associated

# Associated, prime, and irreducible elements.

theorem is_unit.pow {α : Type u_1} [monoid α] {a : α} (n : ) :
is_unit (a ^ n)

theorem is_unit_iff_dvd_one {α : Type u_1} [comm_monoid α] {x : α} :
x 1

theorem is_unit_iff_forall_dvd {α : Type u_1} [comm_monoid α] {x : α} :
∀ (y : α), x y

theorem is_unit_of_dvd_unit {α : Type u_1} [comm_monoid α] {x y : α} :
x y

theorem is_unit_int {n : } :

theorem is_unit_of_dvd_one {α : Type u_1} [comm_monoid α] (a : α) :
a 1

theorem dvd_and_not_dvd_iff {α : Type u_1} {x y : α} :
x y ¬y x y

theorem pow_dvd_pow_iff {α : Type u_1} {x : α} {n m : } :
x 0¬(x ^ n x ^ m n m)

def prime {α : Type u_1}  :
α → Prop

prime element of a comm_monoid_with_zero

Equations
theorem prime.ne_zero {α : Type u_1} {p : α} :
p 0

theorem prime.not_unit {α : Type u_1} {p : α} :
¬

theorem prime.ne_one {α : Type u_1} {p : α} :
p 1

theorem prime.div_or_div {α : Type u_1} {p : α} (hp : prime p) {a b : α} :
p a * bp a p b

theorem prime.dvd_of_dvd_pow {α : Type u_1} {p : α} (hp : prime p) {a : α} {n : } :
p a ^ np a

@[simp]
theorem not_prime_zero {α : Type u_1}  :

@[simp]
theorem not_prime_one {α : Type u_1}  :

theorem exists_mem_multiset_dvd_of_prime {α : Type u_1} {s : multiset α} {p : α} :
p s.prod(∃ (a : α) (H : a s), p a)

theorem left_dvd_or_dvd_right_of_dvd_prime_mul {α : Type u_1} {a b p : α} :
a p * bp a a b

@[class]
def irreducible {α : Type u_1} [monoid α] :
α → Prop

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.

Equations
Instances
theorem irreducible.not_unit {α : Type u_1} [monoid α] {p : α} :
¬

theorem irreducible.is_unit_or_is_unit {α : Type u_1} [monoid α] {p : α} (hp : irreducible p) {a b : α} :
p = a * b

@[simp]
theorem not_irreducible_one {α : Type u_1} [monoid α] :

@[simp]
theorem not_irreducible_zero {α : Type u_1}  :

theorem irreducible.ne_zero {α : Type u_1} {p : α} :
p 0

theorem of_irreducible_mul {α : Type u_1} [monoid α] {x y : α} :
irreducible (x * y)

theorem irreducible_or_factor {α : Type u_1} [monoid α] (x : α) :
¬ ∃ (a b : α), ¬ ¬ a * b = x)

theorem irreducible_of_prime {α : Type u_1} {p : α} :

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} {p : α} (hp : prime p) {a b : α} {k l : } :
p ^ k ap ^ l bp ^ (k + l + 1) a * bp ^ (k + 1) a p ^ (l + 1) b

theorem dvd_symm_of_irreducible {α : Type u_1} [monoid α] {p q : α} :
p qq p

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

theorem dvd_symm_iff_of_irreducible {α : Type u_1} [monoid α] {p q : α} :
(p q q p)

def associated {α : Type u_1} [monoid α] :
α → α → Prop

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

Equations
theorem associated.refl {α : Type u_1} [monoid α] (x : α) :
x

theorem associated.symm {α : Type u_1} [monoid α] {x y : α} :
y x

theorem associated.trans {α : Type u_1} [monoid α] {x y z : α} :
y z z

def associated.setoid (α : Type u_1) [monoid α] :

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

Equations
theorem unit_associated_one {α : Type u_1} [monoid α] {u : units α} :
1

theorem associated_one_iff_is_unit {α : Type u_1} [monoid α] {a : α} :
1

theorem associated_zero_iff_eq_zero {α : Type u_1} (a : α) :
0 a = 0

theorem associated_one_of_mul_eq_one {α : Type u_1} [comm_monoid α] {a : α} (b : α) :
a * b = 1 1

theorem associated_one_of_associated_mul_one {α : Type u_1} [comm_monoid α] {a b : α} :
associated (a * b) 1 1

theorem associated_mul_mul {α : Type u_1} [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
b₁ b₂associated (a₁ * a₂) (b₁ * b₂)

theorem dvd_of_associated {α : Type u_1} [monoid α] {a b : α} :
ba b

theorem dvd_dvd_of_associated {α : Type u_1} [monoid α] {a b : α} :
ba b b a

theorem associated_of_dvd_dvd {α : Type u_1} {a b : α} :
a bb a b

theorem dvd_dvd_iff_associated {α : Type u_1} {a b : α} :
a b b a b

theorem exists_associated_mem_of_dvd_prod {α : Type u_1} {p : α} (hp : prime p) {s : multiset α} :
(∀ (r : α), r sprime r)p s.prod(∃ (q : α) (H : q s), q)

theorem dvd_iff_dvd_of_rel_left {α : Type u_1} {a b c : α} :
b(a c b c)

theorem dvd_iff_dvd_of_rel_right {α : Type u_1} {a b c : α} :
c(a b a c)

theorem eq_zero_iff_of_associated {α : Type u_1} {a b : α} :
b(a = 0 b = 0)

theorem ne_zero_iff_of_associated {α : Type u_1} {a b : α} :
b(a 0 b 0)

theorem prime_of_associated {α : Type u_1} {p q : α} :
q

theorem prime_iff_of_associated {α : Type u_1} {p q : α} :
q(prime p prime q)

theorem is_unit_iff_of_associated {α : Type u_1} [monoid α] {a b : α} :
b(is_unit a is_unit b)

theorem irreducible_of_associated {α : Type u_1} {p q : α} :
q

theorem irreducible_iff_of_associated {α : Type u_1} {p q : α} :
q

theorem associated_mul_left_cancel {α : Type u_1} {a b c d : α} :
associated (a * b) (c * d) ca 0 d

theorem associated_mul_right_cancel {α : Type u_1} {a b c d : α} :
associated (a * b) (c * d) db 0 c

theorem associated_iff_eq {α : Type u_1} [monoid α] [unique (units α)] {x y : α} :
y x = y

theorem associated_eq_eq {α : Type u_1} [monoid α] [unique (units α)] :

def associates (α : Type u_1) [monoid α] :
Type u_1

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

Equations
def associates.mk {α : Type u_1} [monoid α] :
α →

The canonical quotient map from a monoid α into the associates of α

Equations
@[instance]
def associates.inhabited {α : Type u_1} [monoid α] :

Equations
theorem associates.mk_eq_mk_iff_associated {α : Type u_1} [monoid α] {a b : α} :
b

theorem associates.quotient_mk_eq_mk {α : Type u_1} [monoid α] (a : α) :

theorem associates.quot_mk_eq_mk {α : Type u_1} [monoid α] (a : α) :
quot.mk setoid.r a =

theorem associates.forall_associated {α : Type u_1} [monoid α] {p : → Prop} :
(∀ (a : , p a) ∀ (a : α), p

theorem associates.mk_surjective {α : Type u_1} [monoid α] :

@[instance]
def associates.has_one {α : Type u_1} [monoid α] :

Equations
theorem associates.one_eq_mk_one {α : Type u_1} [monoid α] :

@[instance]
def associates.has_bot {α : Type u_1} [monoid α] :

Equations
theorem associates.exists_rep {α : Type u_1} [monoid α] (a : associates α) :
∃ (a0 : α), = a

@[instance]
def associates.has_mul {α : Type u_1} [comm_monoid α] :

Equations
theorem associates.mk_mul_mk {α : Type u_1} [comm_monoid α] {x y : α} :

@[instance]
def associates.comm_monoid {α : Type u_1} [comm_monoid α] :

Equations
@[instance]
def associates.preorder {α : Type u_1} [comm_monoid α] :

Equations
@[simp]
theorem associates.mk_one {α : Type u_1} [comm_monoid α] :

theorem associates.mk_pow {α : Type u_1} [comm_monoid α] (a : α) (n : ) :

theorem associates.dvd_eq_le {α : Type u_1} [comm_monoid α] :

theorem associates.prod_mk {α : Type u_1} [comm_monoid α] {p : multiset α} :

theorem associates.rel_associated_iff_map_eq_map {α : Type u_1} [comm_monoid α] {p q : multiset α} :

theorem associates.mul_eq_one_iff {α : Type u_1} [comm_monoid α] {x y : associates α} :
x * y = 1 x = 1 y = 1

theorem associates.prod_eq_one_iff {α : Type u_1} [comm_monoid α] {p : multiset (associates α)} :
p.prod = 1 ∀ (a : , a pa = 1

theorem associates.units_eq_one {α : Type u_1} [comm_monoid α] (u : units (associates α)) :
u = 1

@[instance]
def associates.unique_units {α : Type u_1} [comm_monoid α] :

Equations
theorem associates.coe_unit_eq_one {α : Type u_1} [comm_monoid α] (u : units (associates α)) :
u = 1

theorem associates.is_unit_iff_eq_one {α : Type u_1} [comm_monoid α] (a : associates α) :
a = 1

theorem associates.is_unit_mk {α : Type u_1} [comm_monoid α] {a : α} :

theorem associates.mul_mono {α : Type u_1} [comm_monoid α] {a b c d : associates α} :
a bc da * c b * d

theorem associates.one_le {α : Type u_1} [comm_monoid α] {a : associates α} :
1 a

theorem associates.prod_le_prod {α : Type u_1} [comm_monoid α] {p q : multiset (associates α)} :
p qp.prod q.prod

theorem associates.le_mul_right {α : Type u_1} [comm_monoid α] {a b : associates α} :
a a * b

theorem associates.le_mul_left {α : Type u_1} [comm_monoid α] {a b : associates α} :
a b * a

@[instance]
def associates.has_zero {α : Type u_1} [has_zero α] [monoid α] :

Equations
@[instance]
def associates.has_top {α : Type u_1} [has_zero α] [monoid α] :

Equations
@[simp]
theorem associates.mk_eq_zero {α : Type u_1} {a : α} :
a = 0

@[instance]
def associates.comm_monoid_with_zero {α : Type u_1}  :

Equations
@[instance]
def associates.nontrivial {α : Type u_1} [nontrivial α] :

theorem associates.exists_non_zero_rep {α : Type u_1} {a : associates α} :
a 0(∃ (a0 : α), a0 0 = a)

theorem associates.dvd_of_mk_le_mk {α : Type u_1} {a b : α} :
a b

theorem associates.mk_le_mk_of_dvd {α : Type u_1} {a b : α} :
a b

theorem associates.mk_le_mk_iff_dvd_iff {α : Type u_1} {a b : α} :
a b

theorem associates.mk_dvd_mk {α : Type u_1} {a b : α} :
a b

theorem associates.prime.le_or_le {α : Type u_1} {p : associates α} (hp : prime p) {a b : associates α} :
p a * bp a p b

theorem associates.exists_mem_multiset_le_of_prime {α : Type u_1} {s : multiset (associates α)} {p : associates α} :
p s.prod(∃ (a : (H : a s), p a)

theorem associates.prime_mk {α : Type u_1} (p : α) :

theorem associates.irreducible_mk {α : Type u_1} (a : α) :

theorem associates.mk_dvd_not_unit_mk_iff {α : Type u_1} {a b : α} :
b

theorem associates.dvd_not_unit_of_lt {α : Type u_1} {a b : associates α} :
a < b b

@[instance]
def associates.partial_order {α : Type u_1}  :

Equations
@[instance]
def associates.order_bot {α : Type u_1}  :

Equations
@[instance]
def associates.order_top {α : Type u_1}  :

Equations
@[instance]
def associates.no_zero_divisors {α : Type u_1}  :

theorem associates.irreducible_iff_prime_iff {α : Type u_1}  :
(∀ (a : α), prime a) ∀ (a : ,

theorem associates.eq_of_mul_eq_mul_left {α : Type u_1} (a b c : associates α) :
a 0a * b = a * cb = c

theorem associates.eq_of_mul_eq_mul_right {α : Type u_1} (a b c : associates α) :
b 0a * b = c * ba = c

theorem associates.le_of_mul_le_mul_left {α : Type u_1} (a b c : associates α) :
a 0a * b a * cb c

theorem associates.one_or_eq_of_le_of_prime {α : Type u_1} (p m : associates α) :
m pm = 1 m = p

theorem associates.dvd_not_unit_iff_lt {α : Type u_1} {a b : associates α} :
b a < b