mathlib documentation

algebra.associated

Associated, prime, and irreducible elements. #

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 : α} (xy : x y) (hu : is_unit y) :
theorem is_unit_of_dvd_one {α : Type u_1} [comm_monoid α] (a : α) (H : a 1) :
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 : } (h0 : x 0) (h1 : ¬is_unit x) :
x ^ n x ^ m n m
def prime {α : Type u_1} [comm_monoid_with_zero α] (p : α) :
Prop

prime element of a comm_monoid_with_zero

Equations
theorem prime.ne_zero {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p 0
theorem prime.not_unit {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
theorem prime.ne_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p 1
theorem prime.div_or_div {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) {a b : α} (h : p a * b) :
p a p b
theorem prime.dvd_of_dvd_pow {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) {a : α} {n : } (h : p a ^ n) :
p 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 : α} (hp : prime p) :
p 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]
structure irreducible {α : Type u_1} [monoid α] (p : α) :
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.

Instances
theorem irreducible.not_unit {α : Type u_1} [monoid α] {p : α} (hp : irreducible p) :
theorem irreducible.is_unit_or_is_unit {α : Type u_1} [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
theorem irreducible_iff {α : Type u_1} [monoid α] {p : α} :
irreducible p ¬is_unit 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 : α) (h : ¬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 : α} (hp : prime 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 : α} (hp : irreducible p) (hq : irreducible 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 : α} (hp : irreducible p) (hq : irreducible q) :
p q q p
def associated {α : Type u_1} [monoid α] (x y : α) :
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 : α) (hab : a * b = 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 associated_pow_pow {α : Type u_1} [comm_monoid α] {a b : α} {n : } (h : associated a b) :
associated (a ^ n) (b ^ n)
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 : α} (h : associated a b) :
a b b a
theorem associated_of_dvd_dvd {α : Type u_1} [cancel_monoid_with_zero α] {a b : α} (hab : a b) (hba : b a) :
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} [monoid α] {a b c : α} (h : associated a b) :
a c b c
theorem dvd_iff_dvd_of_rel_right {α : Type u_1} [monoid α] {a b c : α} (h : associated b c) :
a b a c
theorem eq_zero_iff_of_associated {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a = 0 b = 0
theorem ne_zero_iff_of_associated {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a 0 b 0
theorem prime_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) (hp : prime p) :
theorem associated_of_irreducible_of_dvd {α : Type u_1} [cancel_monoid_with_zero α] {p q : α} (p_irr : irreducible p) (q_irr : irreducible q) (dvd : p q) :
theorem associated_of_prime_of_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] {p q : α} (p_prime : prime p) (q_prime : prime q) (dvd : p q) :
theorem prime_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) :
theorem is_unit_iff_of_associated {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
theorem irreducible_of_associated {α : Type u_1} [monoid α] {p q : α} (h : associated p q) (hp : irreducible p) :
theorem irreducible_iff_of_associated {α : Type u_1} [monoid α] {p q : α} (h : associated p q) :
theorem associated_mul_left_cancel {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b c d : α} (h : associated (a * b) (c * d)) (h₁ : associated a c) (ha : a 0) :
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 α] (a : α) :

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 α] :
@[simp]
theorem associates.associated_map_mk {α : Type u_1} [comm_monoid α] {f : associates α →* α} (hinv : function.right_inverse f associates.mk) (a : α) :
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 α} (h₁ : a b) (h₂ : c d) :
a * 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 α)} (h : p q) :
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 α} (h : p a * b) :
p a p b
theorem associates.exists_mem_multiset_le_of_prime {α : Type u_1} [comm_monoid_with_zero α] {s : multiset (associates α)} {p : associates α} (hp : prime p) :
p 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 α} (hlt : 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 α) (ha : a 0) :
a * 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