mathlib documentation

algebra.associated

Associated, prime, and irreducible elements.

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

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

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

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

theorem is_unit_int {n : } :

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

theorem dvd_and_not_dvd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] {x y : α} :

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

def prime {α : Type u_1} [comm_monoid_with_zero α] :
α → Prop

prime element of a comm_monoid_with_zero

Equations
theorem prime.ne_zero {α : Type u_1} [comm_monoid_with_zero α] {p : α} :
prime pp 0

theorem prime.not_unit {α : Type u_1} [comm_monoid_with_zero α] {p : α} :

theorem prime.ne_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} :
prime pp 1

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

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

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

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

theorem exists_mem_multiset_dvd_of_prime {α : Type u_1} [comm_monoid_with_zero α] {s : multiset α} {p : α} :
prime pp s.prod(∃ (a : α) (H : a s), p a)

theorem left_dvd_or_dvd_right_of_dvd_prime_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b p : α} :
prime pa 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 * bis_unit a is_unit b

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

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

theorem irreducible.ne_zero {α : Type u_1} [monoid_with_zero α] {p : α} :
irreducible pp 0

theorem of_irreducible_mul {α : Type u_1} [monoid α] {x y : α} :

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

theorem irreducible_of_prime {α : Type u_1} [comm_cancel_monoid_with_zero α] {p : α} :

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] {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 : α} :
irreducible pirreducible qp 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 : α} :
irreducible pirreducible 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 : α) :

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

theorem associated.trans {α : Type u_1} [monoid α] {x y z : α} :
associated x yassociated y zassociated x 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 α} :

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

theorem associated_zero_iff_eq_zero {α : Type u_1} [monoid_with_zero α] (a : α) :
associated a 0 a = 0

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

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

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

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

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

theorem associated_of_dvd_dvd {α : Type u_1} [cancel_monoid_with_zero α] {a b : α} :
a bb aassociated a b

theorem dvd_dvd_iff_associated {α : Type u_1} [cancel_monoid_with_zero α] {a b : α} :
a b b a associated a b

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

theorem dvd_iff_dvd_of_rel_left {α : Type u_1} [comm_monoid_with_zero α] {a b c : α} :
associated a b(a c b c)

theorem dvd_iff_dvd_of_rel_right {α : Type u_1} [comm_monoid_with_zero α] {a b c : α} :
associated b c(a b a c)

theorem eq_zero_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :
associated a b(a = 0 b = 0)

theorem ne_zero_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :
associated a b(a 0 b 0)

theorem prime_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} :
associated p qprime pprime q

theorem prime_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} :
associated p q(prime p prime q)

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

theorem irreducible_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} :

theorem irreducible_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} :

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

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

theorem associated_iff_eq {α : Type u_1} [monoid α] [unique (units α)] {x y : α} :
associated x 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 α] :
α → associates α

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 : α} :

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

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

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

@[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 : α), associates.mk 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.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 : associates α), 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 α) :
is_unit a 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} [comm_monoid_with_zero α] {a : α} :

@[instance]

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

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

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

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

theorem associates.prime.le_or_le {α : Type u_1} [comm_monoid_with_zero α] {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} [comm_monoid_with_zero α] {s : multiset (associates α)} {p : associates α} :
prime pp s.prod(∃ (a : associates α) (H : a s), p a)

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

theorem associates.dvd_not_unit_of_lt {α : Type u_1} [comm_monoid_with_zero α] {a b : associates α} :
a < bdvd_not_unit a b

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

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

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

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

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