mathlib documentation

algebra.associated

Associated, prime, and irreducible elements. #

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_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} [cancel_comm_monoid_with_zero α] {x y : α} :
x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit x y
source
theorem pow_dvd_pow_iff {α : Type u_1} [cancel_comm_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.not_dvd_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
¬p ∣ 1
source
theorem prime.ne_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p ≠ 1
source
theorem prime.dvd_or_dvd {α : 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 prime.left_dvd_or_dvd_right_of_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) {a b : α} :
a ∣ p * b → p ∣ a ∨ a ∣ b
source
@[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.

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
theorem irreducible_iff {α : Type u_1} [monoid α] {p : α} :
irreducible p ↔ ¬is_unit p ∧ ∀ (a b : α), 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 : α} :
irreducible p → p ≠ 0
source
theorem of_irreducible_mul {α : Type u_1} [monoid α] {x y : α} :
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
@[protected]
theorem prime.irreducible {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) :
irreducible p
source
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) {a b : α} {k l : ℕ} :
p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b
source
theorem irreducible.dvd_symm {α : Type u_1} [monoid α] {p q : α} (hp : irreducible p) (hq : irreducible q) :
p ∣ q → q ∣ p

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

source
theorem irreducible.dvd_comm {α : 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
@[protected]
theorem associated.refl {α : Type u_1} [monoid α] (x : α) :
associated x x
source
@[protected]
theorem associated.symm {α : Type u_1} [monoid α] {x y : α} :
associated x y → associated y x
source
@[protected]
theorem associated.trans {α : Type u_1} [monoid α] {x y z : α} :
associated x y → associated y z → associated x z
source
@[protected]
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 : α} :
associated (a * b) 1 → associated a 1
source
theorem associated_mul_unit_left {β : Type u_1} [monoid β] (a u : β) (hu : is_unit u) :
associated (a * u) a
source
theorem associated_unit_mul_left {β : Type u_1} [comm_monoid β] (a u : β) (hu : is_unit u) :
associated (u * a) a
source
theorem associated_mul_unit_right {β : Type u_1} [monoid β] (a u : β) (hu : is_unit u) :
associated a (a * u)
source
theorem associated_unit_mul_right {β : Type u_1} [comm_monoid β] (a u : β) (hu : is_unit u) :
associated a (u * a)
source
theorem associated.mul_mul {α : Type u_1} [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
associated a₁ b₁ → associated a₂ b₂ → associated (a₁ * a₂) (b₁ * b₂)
source
theorem associated.mul_left {α : Type u_1} [comm_monoid α] (a : α) {b c : α} (h : associated b c) :
associated (a * b) (a * c)
source
theorem associated.mul_right {α : Type u_1} [comm_monoid α] {a b : α} (h : associated a b) (c : α) :
associated (a * c) (b * c)
source
theorem associated.pow_pow {α : Type u_1} [comm_monoid α] {a b : α} {n : ℕ} (h : associated a b) :
associated (a ^ n) (b ^ n)
source
@[protected]
theorem associated.dvd {α : Type u_1} [monoid α] {a b : α} :
associated a b → a ∣ b
source
@[protected]
theorem associated.dvd_dvd {α : 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 associated.dvd_iff_dvd_left {α : Type u_1} [monoid α] {a b c : α} (h : associated a b) :
a ∣ c ↔ b ∣ c
source
theorem associated.dvd_iff_dvd_right {α : Type u_1} [monoid α] {a b c : α} (h : associated b c) :
a ∣ b ↔ a ∣ c
source
theorem associated.eq_zero_iff {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a = 0 ↔ b = 0
source
theorem associated.ne_zero_iff {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a ≠ 0 ↔ b ≠ 0
source
@[protected]
theorem associated.prime {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) (hp : prime p) :
prime q
source
theorem irreducible.associated_of_dvd {α : Type u_1} [cancel_monoid_with_zero α] {p q : α} (p_irr : irreducible p) (q_irr : irreducible q) (dvd : p ∣ q) :
associated p q
source
theorem irreducible.dvd_irreducible_iff_associated {α : Type u_1} [cancel_monoid_with_zero α] {p q : α} (pp : irreducible p) (qp : irreducible q) :
p ∣ q ↔ associated p q
source
theorem prime.associated_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] {p q : α} (p_prime : prime p) (q_prime : prime q) (dvd : p ∣ q) :
associated p q
source
theorem prime.dvd_prime_iff_associated {α : Type u_1} [cancel_comm_monoid_with_zero α] {p q : α} (pp : prime p) (qp : prime q) :
p ∣ q ↔ associated p q
source
theorem associated.prime_iff {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) :
prime p ↔ prime q
source
@[protected]
theorem associated.is_unit {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
is_unit a → is_unit b
source
theorem associated.is_unit_iff {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
is_unit a ↔ is_unit b
source
@[protected]
theorem associated.irreducible {α : Type u_1} [monoid α] {p q : α} (h : associated p q) (hp : irreducible p) :
irreducible q
source
@[protected]
theorem associated.irreducible_iff {α : Type u_1} [monoid α] {p q : α} (h : associated p q) :
irreducible p ↔ irreducible q
source
theorem associated.of_mul_left {α : Type u_1} [cancel_comm_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.of_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b c d : α} :
associated (a * b) (c * d) → associated b d → b ≠ 0 → associated a c
source
theorem units_eq_one {α : Type u_1} [monoid α] [unique (units α)] (u : units α) :
u = 1
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
@[protected]
def associates.mk {α : Type u_1} [monoid α] (a : α) :
associates α

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

Equations
source
@[protected, 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
@[protected, 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
@[protected, 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
@[protected, instance]
def associates.unique {α : Type u_1} [monoid α] [subsingleton α] :
unique (associates α)
Equations
source
@[protected, 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
@[protected, instance]
def associates.comm_monoid {α : Type u_1} [comm_monoid α] :
comm_monoid (associates α)
Equations
source
@[protected, 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
@[protected]
def associates.mk_monoid_hom {α : Type u_1} [comm_monoid α] :
α →* associates α

associates.mk as a monoid_hom.

Equations
source
@[simp]
theorem associates.mk_monoid_hom_apply {α : Type u_1} [comm_monoid α] (a : α) :
⇑associates.mk_monoid_hom a = associates.mk a
source
theorem associates.associated_map_mk {α : Type u_1} [comm_monoid α] {f : associates α →* α} (hinv : function.right_inverse ⇑f associates.mk) (a : α) :
associated a (⇑f (associates.mk a))
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.mul_eq_one_iff {α : Type u_1} [comm_monoid α] {x y : associates α} :
x * y = 1 ↔ x = 1 ∧ y = 1
source
theorem associates.units_eq_one {α : Type u_1} [comm_monoid α] (u : units (associates α)) :
u = 1
source
@[protected, 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.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
@[protected, instance]
def associates.order_bot {α : Type u_1} [comm_monoid α] :
order_bot (associates α)
Equations
source
@[protected, instance]
def associates.has_zero {α : Type u_1} [has_zero α] [monoid α] :
has_zero (associates α)
Equations
source
@[protected, 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
theorem associates.mk_ne_zero {α : Type u_1} [comm_monoid_with_zero α] {a : α} :
associates.mk a ≠ 0 ↔ a ≠ 0
source
@[protected, instance]
def associates.comm_monoid_with_zero {α : Type u_1} [comm_monoid_with_zero α] :
comm_monoid_with_zero (associates α)
Equations
source
@[protected, instance]
def associates.order_top {α : Type u_1} [comm_monoid_with_zero α] :
order_top (associates α)
Equations
source
@[protected, instance]
def associates.bounded_order {α : Type u_1} [comm_monoid_with_zero α] :
bounded_order (associates α)
Equations
source
@[protected, 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 ≠ 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 : α} :
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 ∣ 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.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
@[protected, instance]
def associates.partial_order {α : Type u_1} [cancel_comm_monoid_with_zero α] :
partial_order (associates α)
Equations
source
@[protected, instance]
def associates.no_zero_divisors {α : Type u_1} [cancel_comm_monoid_with_zero α] :
no_zero_divisors (associates α)
source
theorem associates.irreducible_iff_prime_iff {α : Type u_1} [cancel_comm_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} [cancel_comm_monoid_with_zero α] (a b c : associates α) :
a ≠ 0 → a * b = a * c → b = c
source
theorem associates.eq_of_mul_eq_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] (a b c : associates α) :
b ≠ 0 → a * b = c * b → a = c
source
theorem associates.le_of_mul_le_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] (a b c : associates α) (ha : a ≠ 0) :
a * b ≤ a * c → b ≤ c
source
theorem associates.one_or_eq_of_le_of_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] (p m : associates α) :
prime p → m ≤ p → m = 1 ∨ m = p
source
@[protected, instance]
def associates.cancel_comm_monoid_with_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] :
cancel_comm_monoid_with_zero (associates α)
Equations
source
theorem associates.dvd_not_unit_iff_lt {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b : associates α} :
dvd_not_unit a b ↔ a < b