mathlib3 documentation

algebra.associated

Associated, prime, and irreducible elements. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.not_dvd_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
¬p 1
theorem prime.ne_one {α : Type u_1} [comm_monoid_with_zero α] {p : α} (hp : prime p) :
p 1
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
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 comap_prime {α : Type u_1} {β : Type u_2} [comm_monoid_with_zero α] [comm_monoid_with_zero β] {F : Type u_5} {G : Type u_6} [monoid_with_zero_hom_class F α β] [mul_hom_class G β α] (f : F) (g : G) {p : α} (hinv : (a : α), g (f a) = a) (hp : prime (f p)) :
theorem mul_equiv.prime_iff {α : Type u_1} {β : Type u_2} [comm_monoid_with_zero α] [comm_monoid_with_zero β] {p : α} (e : α ≃* β) :
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
theorem prime.pow_dvd_of_dvd_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] {p a b : α} (hp : prime p) (n : ) (h : ¬p a) (h' : p ^ n a * b) :
p ^ n b
theorem prime.pow_dvd_of_dvd_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] {p a b : α} (hp : prime p) (n : ) (h : ¬p b) (h' : p ^ n a * b) :
p ^ n a
theorem prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] {p a b : α} {n : } (hp : prime p) (hpow : p ^ n.succ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 b) :
p a
theorem prime_pow_succ_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] {p x y : α} (h : prime p) {i : } (hxy : p ^ (i + 1) x * y) :
p ^ (i + 1) x p y
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.

theorem irreducible.not_dvd_one {α : Type u_1} [comm_monoid α] {p : α} (hp : irreducible p) :
¬p 1
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 * b is_unit a is_unit b
@[simp]
theorem not_irreducible_one {α : Type u_1} [monoid α] :
theorem irreducible.ne_one {α : Type u_1} [monoid α] {p : α} :
@[simp]
theorem irreducible.ne_zero {α : Type u_1} [monoid_with_zero α] {p : α} :
theorem of_irreducible_mul {α : Type u_1} [monoid α] {x y : α} :
theorem of_irreducible_pow {α : Type u_1} [monoid α] {x : α} {n : } (hn : n 1) :
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.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.

theorem irreducible.dvd_comm {α : Type u_1} [monoid α] {p q : α} (hp : irreducible p) (hq : irreducible q) :
p q q p
theorem irreducible_units_mul {α : Type u_1} [monoid α] (a : αˣ) (b : α) :
theorem irreducible_is_unit_mul {α : Type u_1} [monoid α] {a b : α} (h : is_unit a) :
theorem irreducible_mul_units {α : Type u_1} [monoid α] (a : αˣ) (b : α) :
theorem irreducible_mul_is_unit {α : Type u_1} [monoid α] {a b : α} (h : is_unit a) :
theorem irreducible_mul_iff {α : Type u_1} [monoid α] {a b : α} :
theorem irreducible.not_square {α : Type u_1} [comm_monoid α] {a : α} (ha : irreducible a) :
theorem is_square.not_irreducible {α : Type u_1} [comm_monoid α] {a : α} (ha : is_square a) :
@[protected]
theorem prime.irreducible {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) :
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
theorem prime.not_square {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) :
theorem is_square.not_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {a : α} (ha : is_square a) :
theorem pow_not_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {a : α} {n : } (hn : n 1) :
¬prime (a ^ n)
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
Instances for associated
@[protected, refl]
theorem associated.refl {α : Type u_1} [monoid α] (x : α) :
@[protected, instance]
def associated.is_refl {α : Type u_1} [monoid α] :
@[protected, symm]
theorem associated.symm {α : Type u_1} [monoid α] {x y : α} :
@[protected, instance]
def associated.is_symm {α : Type u_1} [monoid α] :
@[protected]
theorem associated.comm {α : Type u_1} [monoid α] {x y : α} :
@[protected, trans]
theorem associated.trans {α : Type u_1} [monoid α] {x y z : α} :
@[protected, instance]
def associated.is_trans {α : Type u_1} [monoid α] :
@[protected]
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 : αˣ} :
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 : α} :
theorem associated_mul_unit_left {β : Type u_1} [monoid β] (a u : β) (hu : is_unit u) :
associated (a * u) a
theorem associated_unit_mul_left {β : Type u_1} [comm_monoid β] (a u : β) (hu : is_unit u) :
associated (u * a) a
theorem associated_mul_unit_right {β : Type u_1} [monoid β] (a u : β) (hu : is_unit u) :
associated a (a * u)
theorem associated_unit_mul_right {β : Type u_1} [comm_monoid β] (a u : β) (hu : is_unit u) :
associated a (u * a)
theorem associated_mul_is_unit_left_iff {β : Type u_1} [monoid β] {a u b : β} (hu : is_unit u) :
theorem associated_is_unit_mul_left_iff {β : Type u_1} [comm_monoid β] {u a b : β} (hu : is_unit u) :
theorem associated_mul_is_unit_right_iff {β : Type u_1} [monoid β] {a b u : β} (hu : is_unit u) :
theorem associated_is_unit_mul_right_iff {β : Type u_1} [comm_monoid β] {a u b : β} (hu : is_unit u) :
@[simp]
theorem associated_mul_unit_left_iff {β : Type u_1} [monoid β] {a b : β} {u : βˣ} :
@[simp]
theorem associated_unit_mul_left_iff {β : Type u_1} [comm_monoid β] {a b : β} {u : βˣ} :
@[simp]
theorem associated_mul_unit_right_iff {β : Type u_1} [monoid β] {a b : β} {u : βˣ} :
@[simp]
theorem associated_unit_mul_right_iff {β : Type u_1} [comm_monoid β] {a b : β} {u : βˣ} :
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.mul_left {α : Type u_1} [comm_monoid α] (a : α) {b c : α} (h : associated b c) :
associated (a * b) (a * c)
theorem associated.mul_right {α : Type u_1} [comm_monoid α] {a b : α} (h : associated a b) (c : α) :
associated (a * c) (b * c)
theorem associated.pow_pow {α : Type u_1} [comm_monoid α] {a b : α} {n : } (h : associated a b) :
associated (a ^ n) (b ^ n)
@[protected]
theorem associated.dvd {α : Type u_1} [monoid α] {a b : α} :
@[protected]
theorem associated.dvd_dvd {α : 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 associated.dvd_iff_dvd_left {α : Type u_1} [monoid α] {a b c : α} (h : associated a b) :
a c b c
theorem associated.dvd_iff_dvd_right {α : Type u_1} [monoid α] {a b c : α} (h : associated b c) :
a b a c
theorem associated.eq_zero_iff {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a = 0 b = 0
theorem associated.ne_zero_iff {α : Type u_1} [monoid_with_zero α] {a b : α} (h : associated a b) :
a 0 b 0
@[protected]
theorem associated.prime {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) (hp : prime p) :
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) :
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) :
theorem prime.dvd_prime_iff_associated {α : Type u_1} [cancel_comm_monoid_with_zero α] {p q : α} (pp : prime p) (qp : prime q) :
theorem associated.prime_iff {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (h : associated p q) :
@[protected]
theorem associated.is_unit {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
theorem associated.is_unit_iff {α : Type u_1} [monoid α] {a b : α} (h : associated a b) :
@[protected]
theorem associated.irreducible {α : Type u_1} [monoid α] {p q : α} (h : associated p q) (hp : irreducible p) :
@[protected]
theorem associated.irreducible_iff {α : Type u_1} [monoid α] {p q : α} (h : associated p q) :
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) :
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
theorem associated.of_pow_associated_of_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {p₁ p₂ : α} {k₁ k₂ : } (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : associated (p₁ ^ k₁) (p₂ ^ k₂)) :
associated p₁ p₂
theorem associated.of_pow_associated_of_prime' {α : Type u_1} [cancel_comm_monoid_with_zero α] {p₁ p₂ : α} {k₁ k₂ : } (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₂ : 0 < k₂) (h : associated (p₁ ^ k₁) (p₂ ^ k₂)) :
associated p₁ p₂
theorem units_eq_one {α : Type u_1} [monoid α] [unique αˣ] (u : αˣ) :
u = 1
theorem associated_iff_eq {α : Type u_1} [monoid α] [unique αˣ] {x y : α} :
associated x y x = y
theorem associated_eq_eq {α : Type u_1} [monoid α] [unique αˣ] :
theorem prime_dvd_prime_iff_eq {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique Mˣ] {p q : M} (pp : prime p) (qp : prime q) :
p q p = q
theorem eq_of_prime_pow_eq {R : Type u_5} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : } (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :
p₁ = p₂
theorem eq_of_prime_pow_eq' {R : Type u_5} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : } (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
p₁ = p₂
@[protected]
def associates.mk {α : Type u_1} [monoid α] (a : α) :

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

Equations
@[protected, instance]
def associates.inhabited {α : Type u_1} [monoid α] :
Equations
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)
@[protected, instance]
def associates.has_one {α : Type u_1} [monoid α] :
Equations
@[simp]
theorem associates.mk_one {α : Type u_1} [monoid α] :
theorem associates.one_eq_mk_one {α : Type u_1} [monoid α] :
@[protected, instance]
def associates.has_bot {α : Type u_1} [monoid α] :
Equations
theorem associates.bot_eq_one {α : Type u_1} [monoid α] :
= 1
theorem associates.exists_rep {α : Type u_1} [monoid α] (a : associates α) :
(a0 : α), associates.mk a0 = a
@[protected, instance]
def associates.unique {α : Type u_1} [monoid α] [subsingleton α] :
Equations
@[protected, instance]
def associates.has_mul {α : Type u_1} [comm_monoid α] :
Equations
theorem associates.mk_mul_mk {α : Type u_1} [comm_monoid α] {x y : α} :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem associates.mk_pow {α : Type u_1} [comm_monoid α] (a : α) (n : ) :
theorem associates.mul_eq_one_iff {α : Type u_1} [comm_monoid α] {x y : associates α} :
x * y = 1 x = 1 y = 1
theorem associates.units_eq_one {α : Type u_1} [comm_monoid α] (u : (associates α)ˣ) :
u = 1
@[protected, instance]
Equations
theorem associates.coe_unit_eq_one {α : Type u_1} [comm_monoid α] (u : (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_iff_eq_bot {α : Type u_1} [comm_monoid α] {a : associates α} :
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.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
@[protected, instance]
Equations
theorem associates.dvd_of_mk_le_mk {α : Type u_1} [comm_monoid α] {a b : α} :
theorem associates.mk_le_mk_of_dvd {α : Type u_1} [comm_monoid α] {a b : α} :
theorem associates.mk_dvd_mk {α : Type u_1} [comm_monoid α] {a b : α} :
@[protected, instance]
def associates.has_zero {α : Type u_1} [has_zero α] [monoid α] :
Equations
@[protected, instance]
def associates.has_top {α : Type u_1} [has_zero α] [monoid α] :
Equations
@[simp]
theorem associates.mk_eq_zero {α : Type u_1} [monoid_with_zero α] {a : α} :
theorem associates.mk_ne_zero {α : Type u_1} [monoid_with_zero α] {a : α} :
@[protected, instance]
theorem associates.exists_non_zero_rep {α : Type u_1} [monoid_with_zero α] {a : associates α} :
a 0 ( (a0 : α), a0 0 associates.mk a0 = a)
@[protected, instance]
Equations
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.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.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
theorem associates.le_one_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : associates α} :
p 1 p = 1
theorem dvd_not_unit.not_unit {α : Type u_1} [comm_monoid_with_zero α] {p q : α} (hp : dvd_not_unit p q) :
theorem dvd_not_unit_of_dvd_not_unit_associated {α : Type u_1} [comm_monoid_with_zero α] [nontrivial α] {p q r : α} (h : dvd_not_unit p q) (h' : associated q r) :
theorem is_unit_of_associated_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] {p b : α} (h : associated (p * b) p) (hp : p 0) :
theorem dvd_not_unit.ne {α : Type u_1} [cancel_comm_monoid_with_zero α] {p q : α} (h : dvd_not_unit p q) :
p q
theorem pow_injective_of_not_unit {α : Type u_1} [cancel_comm_monoid_with_zero α] {q : α} (hq : ¬is_unit q) (hq' : q 0) :
function.injective (λ (n : ), q ^ n)
theorem dvd_prime_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] {p q : α} (hp : prime p) (n : ) :
q p ^ n (i : ) (H : i n), associated q (p ^ i)