algebra.associated - mathlib3 docs

source

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

Prop

prime element of a comm_monoid_with_zero

Equations

prime p = (p ≠ 0 ∧ ¬is_unit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b)

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 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)) :

prime p

source

theorem mul_equiv.prime_iff {α : Type u_1} {β : Type u_2} [comm_monoid_with_zero α] [comm_monoid_with_zero β] {p : α} (e : α ≃* β) :

prime p ↔ prime (⇑e p)

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

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

source

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

source

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

source

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

source

structure irreducible {α : Type u_1} [monoid α] (p : α) :

Prop

not_unit : ¬is_unit p
is_unit_or_is_unit' : ∀ (a b : α), p = a * b → is_unit a ∨ is_unit b

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_dvd_one {α : Type u_1} [comm_monoid α] {p : α} (hp : irreducible p) :

¬p ∣ 1

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

theorem irreducible.ne_one {α : Type u_1} [monoid α] {p : α} :

irreducible p → p ≠ 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 of_irreducible_pow {α : Type u_1} [monoid α] {x : α} {n : ℕ} (hn : n ≠ 1) :

irreducible (x ^ n) → is_unit x

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.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

theorem irreducible_units_mul {α : Type u_1} [monoid α] (a : αˣ) (b : α) :

irreducible (↑a * b) ↔ irreducible b

source

theorem irreducible_is_unit_mul {α : Type u_1} [monoid α] {a b : α} (h : is_unit a) :

irreducible (a * b) ↔ irreducible b

source

theorem irreducible_mul_units {α : Type u_1} [monoid α] (a : αˣ) (b : α) :

irreducible (b * ↑a) ↔ irreducible b

source

theorem irreducible_mul_is_unit {α : Type u_1} [monoid α] {a b : α} (h : is_unit a) :

irreducible (b * a) ↔ irreducible b

source

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

irreducible (a * b) ↔ irreducible a ∧ is_unit b ∨ irreducible b ∧ is_unit a

source

theorem irreducible.not_square {α : Type u_1} [comm_monoid α] {a : α} (ha : irreducible a) :

¬is_square a

source

theorem is_square.not_irreducible {α : Type u_1} [comm_monoid α] {a : α} (ha : is_square a) :

¬irreducible a

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 prime.not_square {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) :

¬is_square p

source

theorem is_square.not_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {a : α} (ha : is_square a) :

¬prime a

source

theorem pow_not_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {a : α} {n : ℕ} (hn : n ≠ 1) :

¬prime (a ^ n)

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

associated x y = ∃ (u : αˣ), x * ↑u = y

Instances for associated

source

@[protected, refl]

theorem associated.refl {α : Type u_1} [monoid α] (x : α) :

associated x x

source

@[protected, instance]

def associated.is_refl {α : Type u_1} [monoid α] :

is_refl α associated

source

@[protected, symm]

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

associated x y → associated y x

source

@[protected, instance]

def associated.is_symm {α : Type u_1} [monoid α] :

is_symm α associated

source

@[protected]

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

associated x y ↔ associated y x

source

@[protected, trans]

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

associated x y → associated y z → associated x z

source

@[protected, instance]

def associated.is_trans {α : Type u_1} [monoid α] :

is_trans α associated

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

associated.setoid α = {r := associated _inst_1, iseqv := _}

source

theorem unit_associated_one {α : Type u_1} [monoid α] {u : αˣ} :

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_is_unit_left_iff {β : Type u_1} [monoid β] {a u b : β} (hu : is_unit u) :

associated (a * u) b ↔ associated a b

source

theorem associated_is_unit_mul_left_iff {β : Type u_1} [comm_monoid β] {u a b : β} (hu : is_unit u) :

associated (u * a) b ↔ associated a b

source

theorem associated_mul_is_unit_right_iff {β : Type u_1} [monoid β] {a b u : β} (hu : is_unit u) :

associated a (b * u) ↔ associated a b

source

theorem associated_is_unit_mul_right_iff {β : Type u_1} [comm_monoid β] {a u b : β} (hu : is_unit u) :

associated a (u * b) ↔ associated a b

source

@[simp]

theorem associated_mul_unit_left_iff {β : Type u_1} [monoid β] {a b : β} {u : βˣ} :

associated (a * ↑u) b ↔ associated a b

source

@[simp]

theorem associated_unit_mul_left_iff {β : Type u_1} [comm_monoid β] {a b : β} {u : βˣ} :

associated (↑u * a) b ↔ associated a b

source

@[simp]

theorem associated_mul_unit_right_iff {β : Type u_1} [monoid β] {a b : β} {u : βˣ} :

associated a (b * ↑u) ↔ associated a b

source

@[simp]

theorem associated_unit_mul_right_iff {β : Type u_1} [comm_monoid β] {a b : β} {u : βˣ} :

associated a (↑u * b) ↔ associated a b

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

@[protected, instance]

def associated.decidable_rel {α : Type u_1} [cancel_monoid_with_zero α] [decidable_rel has_dvd.dvd] :

decidable_rel associated

Equations

associated.decidable_rel = λ (a b : α), decidable_of_iff (a ∣ b ∧ b ∣ a) dvd_dvd_iff_associated

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 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₂

source

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₂

source

theorem units_eq_one {α : Type u_1} [monoid α] [unique αˣ] (u : αˣ) :

u = 1

source

theorem associated_iff_eq {α : Type u_1} [monoid α] [unique αˣ] {x y : α} :

associated x y ↔ x = y

source

theorem associated_eq_eq {α : Type u_1} [monoid α] [unique αˣ] :

associated = eq

source

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

source

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₂

source

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₂

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