mathlib documentation

algebra.associated

Associated, prime, and irreducible elements.

source
theorem is_unit_pow {α : Type u_1} [monoid α] {a : α} (n : ℕ) (a_1 : is_unit a) :
is_unit (a ^ n)

source
theorem is_unit_iff_dvd_one {α : Type u_1} [comm_monoid α] {x : α} :
is_unit x ↔ x ∣ 1

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

source
theorem is_unit_of_dvd_unit {α : Type u_1} [comm_monoid α] {x y : α} (xy : x ∣ y) (hu : is_unit y) :
is_unit x

source
theorem is_unit_int {n : ℤ} :
is_unit n ↔ n.nat_abs = 1

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

source
theorem dvd_and_not_dvd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] {x y : α} :
x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit x y

source
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

source
def prime {α : Type u_1} [comm_monoid_with_zero α] (p : α) :
Prop

prime element of a comm_monoid_with_zero

Equations
source
theorem prime.ne_zero {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p ≠ 0

source
theorem prime.not_unit {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
¬is_unit p

source
theorem prime.ne_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p ≠ 1

source
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

source
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

source
@[simp]
theorem not_prime_zero {α : Type u_1} [comm_monoid_with_zero α] :
¬prime 0

source
@[simp]
theorem not_prime_one {α : Type u_1} [comm_monoid_with_zero α] :
¬prime 1

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

source
theorem left_dvd_or_dvd_right_of_dvd_prime_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b p : α} (a_1 : prime p) (a_2 : a ∣ p * b) :
p ∣ a ∨ a ∣ b

source
@[class]
def 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.

Equations
Instances
source
theorem irreducible.not_unit {α : Type u_1} [monoid α] {p : α} (hp : irreducible p) :
¬is_unit p

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

source
@[simp]
theorem not_irreducible_one {α : Type u_1} [monoid α] :
¬irreducible 1

source
@[simp]
theorem not_irreducible_zero {α : Type u_1} [monoid_with_zero α] :
¬irreducible 0

source
theorem irreducible.ne_zero {α : Type u_1} [monoid_with_zero α] {p : α} (a : irreducible p) :
p ≠ 0

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

source
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

source
theorem irreducible_of_prime {α : Type u_1} [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) :
irreducible p

source
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 : ℕ} (a_1 : p ^ k ∣ a) (a_2 : p ^ l ∣ b) (a_3 : p ^ (k + l + 1) ∣ a * b) :
p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b

source
theorem dvd_symm_of_irreducible {α : Type u_1} [monoid α] {p q : α} (hp : irreducible p) (hq : irreducible q) (a : p ∣ q) :
q ∣ p

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

source
theorem dvd_symm_iff_of_irreducible {α : Type u_1} [monoid α] {p q : α} (hp : irreducible p) (hq : irreducible q) :
p ∣ q ↔ q ∣ p

source
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
source
theorem associated.refl {α : Type u_1} [monoid α] (x : α) :
associated x x

source
theorem associated.symm {α : Type u_1} [monoid α] {x y : α} (a : associated x y) :
associated y x

source
theorem associated.trans {α : Type u_1} [monoid α] {x y z : α} (a : associated x y) (a_1 : associated y z) :
associated x z

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

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

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

source
theorem associated_one_iff_is_unit {α : Type u_1} [monoid α] {a : α} :
associated a 1 ↔ is_unit a

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

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

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

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

source
theorem dvd_of_associated {α : Type u_1} [monoid α] {a b : α} (a_1 : associated a b) :
a ∣ b

source
theorem dvd_dvd_of_associated {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
a ∣ b ∧ b ∣ a

source
theorem associated_of_dvd_dvd {α : Type u_1} [cancel_monoid_with_zero α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) :
associated a b

source
theorem dvd_dvd_iff_associated {α : Type u_1} [cancel_monoid_with_zero α] {a b : α} :
a ∣ b ∧ b ∣ a ↔ associated a b

source
theorem exists_associated_mem_of_dvd_prod {α : Type u_1} [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) {s : multiset α} (a : ∀ (r : α), r ∈ s → prime r) (a_1 : p ∣ s.prod) :
∃ (q : α) (H : q ∈ s), associated p q

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

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

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

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

source
theorem prime_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) (hp : prime p) :
prime q

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

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

source
theorem irreducible_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) (hp : irreducible p) :
irreducible q

source
theorem irreducible_iff_of_associated {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) :
irreducible p ↔ irreducible q

source
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) :
associated b d

source
theorem associated_mul_right_cancel {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b c d : α} (a_1 : associated (a * b) (c * d)) (a_2 : associated b d) (a_3 : b ≠ 0) :
associated a c

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

source
theorem associated_eq_eq {α : Type u_1} [monoid α] [unique (units α)] :
associated = eq

source
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
source
def associates.mk {α : Type u_1} [monoid α] (a : α) :
associates α

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

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

Equations
source
theorem associates.mk_eq_mk_iff_associated {α : Type u_1} [monoid α] {a b : α} :
associates.mk a = associates.mk b ↔ associated a b

source
theorem associates.quotient_mk_eq_mk {α : Type u_1} [monoid α] (a : α) :
⟦a⟧ = associates.mk a

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

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

source
theorem associates.mk_surjective {α : Type u_1} [monoid α] :
function.surjective associates.mk

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

Equations
source
theorem associates.one_eq_mk_one {α : Type u_1} [monoid α] :
1 = associates.mk 1

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

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

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

Equations
source
theorem associates.mk_mul_mk {α : Type u_1} [comm_monoid α] {x y : α} :
(associates.mk x) * associates.mk y = associates.mk (x * y)

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

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

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

source
theorem associates.mk_pow {α : Type u_1} [comm_monoid α] (a : α) (n : ℕ) :
associates.mk (a ^ n) = associates.mk a ^ n

source
theorem associates.dvd_eq_le {α : Type u_1} [comm_monoid α] :
has_dvd.dvd = has_le.le

source
theorem associates.prod_mk {α : Type u_1} [comm_monoid α] {p : multiset α} :
(multiset.map associates.mk p).prod = associates.mk p.prod

source
theorem associates.rel_associated_iff_map_eq_map {α : Type u_1} [comm_monoid α] {p q : multiset α} :
multiset.rel associated p q ↔ multiset.map associates.mk p = multiset.map associates.mk q

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

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

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

source
@[instance]
def associates.unique_units {α : Type u_1} [comm_monoid α] :
unique (units (associates α))

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

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

source
theorem associates.is_unit_mk {α : Type u_1} [comm_monoid α] {a : α} :
is_unit (associates.mk a) ↔ is_unit a

source
theorem associates.mul_mono {α : Type u_1} [comm_monoid α] {a b c d : associates α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a * c ≤ b * d

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

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

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

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

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

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

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

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

Equations
source
@[instance]
def associates.nontrivial {α : Type u_1} [comm_monoid_with_zero α] [nontrivial α] :
nontrivial (associates α)

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

source
theorem associates.dvd_of_mk_le_mk {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (a_1 : associates.mk a ≤ associates.mk b) :
a ∣ b

source
theorem associates.mk_le_mk_of_dvd {α : Type u_1} [comm_monoid_with_zero α] {a b : α} (a_1 : a ∣ b) :
associates.mk a ≤ associates.mk b

source
theorem associates.mk_le_mk_iff_dvd_iff {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :
associates.mk a ≤ associates.mk b ↔ a ∣ b

source
theorem associates.mk_dvd_mk {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :
associates.mk a ∣ associates.mk b ↔ a ∣ b

source
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

source
theorem associates.exists_mem_multiset_le_of_prime {α : Type u_1} [comm_monoid_with_zero α] {s : multiset (associates α)} {p : associates α} (hp : prime p) (a : p ≤ s.prod) :
∃ (a : associates α) (H : a ∈ s), p ≤ a

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

source
theorem associates.irreducible_mk {α : Type u_1} [comm_monoid_with_zero α] (a : α) :
irreducible (associates.mk a) ↔ irreducible a

source
theorem associates.mk_dvd_not_unit_mk_iff {α : Type u_1} [comm_monoid_with_zero α] {a b : α} :
dvd_not_unit (associates.mk a) (associates.mk b) ↔ dvd_not_unit a b

source
theorem associates.dvd_not_unit_of_lt {α : Type u_1} [comm_monoid_with_zero α] {a b : associates α} (hlt : a < b) :
dvd_not_unit a b

source
@[instance]
def associates.partial_order {α : Type u_1} [comm_cancel_monoid_with_zero α] :
partial_order (associates α)

Equations
source
@[instance]
def associates.order_bot {α : Type u_1} [comm_cancel_monoid_with_zero α] :
order_bot (associates α)

Equations
source
@[instance]
def associates.order_top {α : Type u_1} [comm_cancel_monoid_with_zero α] :
order_top (associates α)

Equations
source
@[instance]
def associates.no_zero_divisors {α : Type u_1} [comm_cancel_monoid_with_zero α] :
no_zero_divisors (associates α)

source
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

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

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

source
theorem associates.le_of_mul_le_mul_left {α : Type u_1} [comm_cancel_monoid_with_zero α] (a b c : associates α) (ha : a ≠ 0) (a_1 : a * b ≤ a * c) :
b ≤ c

source
theorem associates.one_or_eq_of_le_of_prime {α : Type u_1} [comm_cancel_monoid_with_zero α] (p m : associates α) (a : prime p) (a_1 : m ≤ p) :
m = 1 ∨ m = p

source
@[instance]
def associates.comm_cancel_monoid_with_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] :
comm_cancel_monoid_with_zero (associates α)

Equations
source
theorem associates.dvd_not_unit_iff_lt {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b : associates α} :
dvd_not_unit a b ↔ a < b