Associated, prime, and irreducible elements.

In this file we define the predicate Prime p saying that an element of a commutative monoid with zero is prime. Namely, Prime p means that p isn't zero, it isn't a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;

In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Irreducible, however this is not true in general.

We also define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient.

def Prime {α : Type u_1} [CommMonoidWithZero α] (p : α) : Prop

An element p of a commutative monoid with zero (e.g., a ring) is called prime, if it's not zero, not a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b.

Equations

• Prime p = (p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b)

theorem Prime.ne_zero {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) : p ≠ 0

theorem Prime.not_unit {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) : ¬IsUnit p

theorem Prime.not_dvd_one {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) : ¬p ∣ 1

theorem Prime.ne_one {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) : p ≠ 1

theorem Prime.dvd_or_dvd {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} (h : p ∣ a * b) : p ∣ a ∨ p ∣ b

theorem Prime.dvd_mul {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} : p ∣ a * b ↔ p ∣ a ∨ p ∣ b

theorem Prime.isPrimal {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) : IsPrimal p

theorem Prime.not_dvd_mul {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} (ha : ¬p ∣ a) (hb : ¬p ∣ b) : ¬p ∣ a * b

theorem Prime.dvd_of_dvd_pow {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a

theorem Prime.dvd_pow_iff_dvd {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a

@[simp]

theorem not_prime_zero {α : Type u_1} [CommMonoidWithZero α] : ¬Prime 0

@[simp]

theorem not_prime_one {α : Type u_1} [CommMonoidWithZero α] : ¬Prime 1

theorem comap_prime {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [CommMonoidWithZero β] {F : Type u_5} {G : Type u_6} [FunLike F α β] [MonoidWithZeroHomClass F α β] [FunLike G β α] [MulHomClass G β α] (f : F) (g : G) {p : α} (hinv : ∀ (a : α), g (f a) = a) (hp : Prime (f p)) : Prime p

theorem MulEquiv.prime_iff {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [CommMonoidWithZero β] {p : α} (e : α ≃* β) : Prime p ↔ Prime (e p)

theorem Prime.left_dvd_or_dvd_right_of_dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} : a ∣ p * b → p ∣ a ∨ a ∣ b

theorem Prime.pow_dvd_of_dvd_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] {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} [CancelCommMonoidWithZero α] {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} [CancelCommMonoidWithZero α] {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_5} [CancelCommMonoidWithZero α] {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.

• not_unit : ¬IsUnit p

  p is not a unit

• isUnit_or_isUnit' : ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b

  if p factors then one factor is a unit

theorem Irreducible.not_unit {α : Type u_1} [Monoid α] {p : α} (self : Irreducible p) : ¬IsUnit p

p is not a unit

theorem Irreducible.isUnit_or_isUnit' {α : Type u_1} [Monoid α] {p : α} (self : Irreducible p) (a : α) (b : α) : p = a * b → IsUnit a ∨ IsUnit b

if p factors then one factor is a unit

theorem Irreducible.not_dvd_one {α : Type u_1} [CommMonoid α] {p : α} (hp : Irreducible p) : ¬p ∣ 1

theorem Irreducible.isUnit_or_isUnit {α : Type u_1} [Monoid α] {p : α} (hp : Irreducible p) {a : α} {b : α} (h : p = a * b) : IsUnit a ∨ IsUnit b

theorem irreducible_iff {α : Type u_1} [Monoid α] {p : α} : Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b

@[simp]

theorem not_irreducible_one {α : Type u_1} [Monoid α] : ¬Irreducible 1

theorem Irreducible.ne_one {α : Type u_1} [Monoid α] {p : α} : Irreducible p → p ≠ 1

@[simp]

theorem not_irreducible_zero {α : Type u_1} [MonoidWithZero α] : ¬Irreducible 0

theorem Irreducible.ne_zero {α : Type u_1} [MonoidWithZero α] {p : α} : Irreducible p → p ≠ 0

theorem of_irreducible_mul {α : Type u_5} [Monoid α] {x : α} {y : α} : Irreducible (x * y) → IsUnit x ∨ IsUnit y

theorem not_irreducible_pow {α : Type u_5} [Monoid α] {x : α} {n : ℕ} (hn : n ≠ 1) : ¬Irreducible (x ^ n)

theorem irreducible_or_factor {α : Type u_5} [Monoid α] (x : α) (h : ¬IsUnit x) : Irreducible x ∨ ∃ (a : α), ∃ (b : α), ¬IsUnit a ∧ ¬IsUnit 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 : α) : Irreducible (↑a * b) ↔ Irreducible b

theorem irreducible_isUnit_mul {α : Type u_1} [Monoid α] {a : α} {b : α} (h : IsUnit a) : Irreducible (a * b) ↔ Irreducible b

theorem irreducible_mul_units {α : Type u_1} [Monoid α] (a : αˣ) (b : α) : Irreducible (b * ↑a) ↔ Irreducible b

theorem irreducible_mul_isUnit {α : Type u_1} [Monoid α] {a : α} {b : α} (h : IsUnit a) : Irreducible (b * a) ↔ Irreducible b

theorem irreducible_mul_iff {α : Type u_1} [Monoid α] {a : α} {b : α} : Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

theorem Irreducible.not_square {α : Type u_1} [CommMonoid α] {a : α} (ha : Irreducible a) : ¬IsSquare a

theorem IsSquare.not_irreducible {α : Type u_1} [CommMonoid α] {a : α} (ha : IsSquare a) : ¬Irreducible a

theorem Irreducible.prime_of_isPrimal {α : Type u_1} [CommMonoidWithZero α] {a : α} (irr : Irreducible a) (primal : IsPrimal a) : Prime a

theorem Irreducible.prime {α : Type u_1} [CommMonoidWithZero α] [DecompositionMonoid α] {a : α} (irr : Irreducible a) : Prime a

theorem Prime.irreducible {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) : Irreducible p

theorem irreducible_iff_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecompositionMonoid α] {a : α} : Irreducible a ↔ Prime a

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] {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} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) : ¬IsSquare p

theorem IsSquare.not_prime {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} (ha : IsSquare a) : ¬Prime a

theorem not_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] {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

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

theorem Associated.refl {α : Type u_1} [Monoid α] (x : α) : Associated x x

theorem Associated.rfl {α : Type u_1} [Monoid α] {x : α} : Associated x x

instance Associated.instIsRefl {α : Type u_1} [Monoid α] : IsRefl α Associated

Equations

• ⋯ = ⋯

theorem Associated.symm {α : Type u_1} [Monoid α] {x : α} {y : α} : Associated x y → Associated y x

instance Associated.instIsSymm {α : Type u_1} [Monoid α] : IsSymm α Associated

Equations

• ⋯ = ⋯

theorem Associated.comm {α : Type u_1} [Monoid α] {x : α} {y : α} : Associated x y ↔ Associated y x

theorem Associated.trans {α : Type u_1} [Monoid α] {x : α} {y : α} {z : α} : Associated x y → Associated y z → Associated x z

instance Associated.instIsTrans {α : Type u_1} [Monoid α] : IsTrans α Associated

Equations

• ⋯ = ⋯

def Associated.setoid (α : Type u_5) [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, iseqv := ⋯ }

theorem Associated.map {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] {F : Type u_7} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x : M} {y : M} (ha : Associated x y) : Associated (f x) (f y)

theorem unit_associated_one {α : Type u_1} [Monoid α] {u : αˣ} : Associated (↑u) 1

@[simp]

theorem associated_one_iff_isUnit {α : Type u_1} [Monoid α] {a : α} : Associated a 1 ↔ IsUnit a

@[simp]

theorem associated_zero_iff_eq_zero {α : Type u_1} [MonoidWithZero α] (a : α) : Associated a 0 ↔ a = 0

theorem associated_one_of_mul_eq_one {α : Type u_1} [CommMonoid α] {a : α} (b : α) (hab : a * b = 1) : Associated a 1

theorem associated_one_of_associated_mul_one {α : Type u_1} [CommMonoid α] {a : α} {b : α} : Associated (a * b) 1 → Associated a 1

theorem associated_mul_unit_left {β : Type u_5} [Monoid β] (a : β) (u : β) (hu : IsUnit u) : Associated (a * u) a

theorem associated_unit_mul_left {β : Type u_5} [CommMonoid β] (a : β) (u : β) (hu : IsUnit u) : Associated (u * a) a

theorem associated_mul_unit_right {β : Type u_5} [Monoid β] (a : β) (u : β) (hu : IsUnit u) : Associated a (a * u)

theorem associated_unit_mul_right {β : Type u_5} [CommMonoid β] (a : β) (u : β) (hu : IsUnit u) : Associated a (u * a)

theorem associated_mul_isUnit_left_iff {β : Type u_5} [Monoid β] {a : β} {u : β} {b : β} (hu : IsUnit u) : Associated (a * u) b ↔ Associated a b

theorem associated_isUnit_mul_left_iff {β : Type u_5} [CommMonoid β] {u : β} {a : β} {b : β} (hu : IsUnit u) : Associated (u * a) b ↔ Associated a b

theorem associated_mul_isUnit_right_iff {β : Type u_5} [Monoid β] {a : β} {b : β} {u : β} (hu : IsUnit u) : Associated a (b * u) ↔ Associated a b

theorem associated_isUnit_mul_right_iff {β : Type u_5} [CommMonoid β] {a : β} {u : β} {b : β} (hu : IsUnit u) : Associated a (u * b) ↔ Associated a b

@[simp]

theorem associated_mul_unit_left_iff {β : Type u_5} [Monoid β] {a : β} {b : β} {u : βˣ} : Associated (a * ↑u) b ↔ Associated a b

@[simp]

theorem associated_unit_mul_left_iff {β : Type u_5} [CommMonoid β] {a : β} {b : β} {u : βˣ} : Associated (↑u * a) b ↔ Associated a b

@[simp]

theorem associated_mul_unit_right_iff {β : Type u_5} [Monoid β] {a : β} {b : β} {u : βˣ} : Associated a (b * ↑u) ↔ Associated a b

@[simp]

theorem associated_unit_mul_right_iff {β : Type u_5} [CommMonoid β] {a : β} {b : β} {u : βˣ} : Associated a (↑u * b) ↔ Associated a b

theorem Associated.mul_left {α : Type u_1} [Monoid α] (a : α) {b : α} {c : α} (h : Associated b c) : Associated (a * b) (a * c)

theorem Associated.mul_right {α : Type u_1} [CommMonoid α] {a : α} {b : α} (h : Associated a b) (c : α) : Associated (a * c) (b * c)

theorem Associated.mul_mul {α : Type u_1} [CommMonoid α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : Associated a₁ b₁) (h₂ : Associated a₂ b₂) : Associated (a₁ * a₂) (b₁ * b₂)

theorem Associated.pow_pow {α : Type u_1} [CommMonoid α] {a : α} {b : α} {n : ℕ} (h : Associated a b) : Associated (a ^ n) (b ^ n)

theorem Associated.dvd {α : Type u_1} [Monoid α] {a : α} {b : α} : Associated a b → a ∣ b

theorem Associated.dvd' {α : Type u_1} [Monoid α] {a : α} {b : α} (h : Associated a b) : b ∣ a

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} [CancelMonoidWithZero α] {a : α} {b : α} (hab : a ∣ b) (hba : b ∣ a) : Associated a b

theorem dvd_dvd_iff_associated {α : Type u_1} [CancelMonoidWithZero α] {a : α} {b : α} : a ∣ b ∧ b ∣ a ↔ Associated a b

instance instDecidableRelAssociatedOfDvd {α : Type u_1} [CancelMonoidWithZero α] [DecidableRel fun (x1 x2 : α) => x1 ∣ x2] : DecidableRel fun (x1 x2 : α) => Associated x1 x2

Equations

• instDecidableRelAssociatedOfDvd x✝ x = decidable_of_iff (x✝ ∣ x ∧ x ∣ x✝) ⋯

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} [MonoidWithZero α] {a : α} {b : α} (h : Associated a b) : a = 0 ↔ b = 0

theorem Associated.ne_zero_iff {α : Type u_1} [MonoidWithZero α] {a : α} {b : α} (h : Associated a b) : a ≠ 0 ↔ b ≠ 0

theorem Associated.neg_left {α : Type u_1} [Monoid α] [HasDistribNeg α] {a : α} {b : α} (h : Associated a b) : Associated (-a) b

theorem Associated.neg_right {α : Type u_1} [Monoid α] [HasDistribNeg α] {a : α} {b : α} (h : Associated a b) : Associated a (-b)

theorem Associated.neg_neg {α : Type u_1} [Monoid α] [HasDistribNeg α] {a : α} {b : α} (h : Associated a b) : Associated (-a) (-b)

theorem Associated.prime {α : Type u_1} [CommMonoidWithZero α] {p : α} {q : α} (h : Associated p q) (hp : Prime p) : Prime q

theorem prime_mul_iff {α : Type u_1} [CancelCommMonoidWithZero α] {x : α} {y : α} : Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

@[simp]

theorem prime_pow_iff {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {n : ℕ} : Prime (p ^ n) ↔ Prime p ∧ n = 1

theorem Irreducible.dvd_iff {α : Type u_1} [Monoid α] {x : α} {y : α} (hx : Irreducible x) : y ∣ x ↔ IsUnit y ∨ Associated x y

theorem Irreducible.associated_of_dvd {α : Type u_1} [Monoid α] {p : α} {q : α} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p ∣ q) : Associated p q

theorem Irreducible.dvd_irreducible_iff_associated {α : Type u_1} [Monoid α] {p : α} {q : α} (pp : Irreducible p) (qp : Irreducible q) : p ∣ q ↔ Associated p q

theorem Prime.associated_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {q : α} (p_prime : Prime p) (q_prime : Prime q) (dvd : p ∣ q) : Associated p q

theorem Prime.dvd_prime_iff_associated {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {q : α} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ Associated p q

theorem Associated.prime_iff {α : Type u_1} [CommMonoidWithZero α] {p : α} {q : α} (h : Associated p q) : Prime p ↔ Prime q

theorem Associated.isUnit {α : Type u_1} [Monoid α] {a : α} {b : α} (h : Associated a b) : IsUnit a → IsUnit b

theorem Associated.isUnit_iff {α : Type u_1} [Monoid α] {a : α} {b : α} (h : Associated a b) : IsUnit a ↔ IsUnit b

theorem Irreducible.isUnit_iff_not_associated_of_dvd {α : Type u_1} [Monoid α] {x : α} {y : α} (hx : Irreducible x) (hy : y ∣ x) : IsUnit y ↔ ¬Associated x y

theorem Associated.irreducible {α : Type u_1} [Monoid α] {p : α} {q : α} (h : Associated p q) (hp : Irreducible p) : Irreducible q

theorem Associated.irreducible_iff {α : Type u_1} [Monoid α] {p : α} {q : α} (h : Associated p q) : Irreducible p ↔ Irreducible q

theorem Associated.of_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {b : α} {c : α} {d : α} (h : Associated (a * b) (c * d)) (h₁ : Associated a c) (ha : a ≠ 0) : Associated b d

theorem Associated.of_mul_right {α : Type u_1} [CancelCommMonoidWithZero α] {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} [CancelCommMonoidWithZero α] {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} [CancelCommMonoidWithZero α] {p₁ : α} {p₂ : α} {k₁ : ℕ} {k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₂ : 0 < k₂) (h : Associated (p₁ ^ k₁) (p₂ ^ k₂)) : Associated p₁ p₂

theorem Irreducible.isRelPrime_iff_not_dvd {α : Type u_1} [Monoid α] {p : α} {n : α} (hp : Irreducible p) : IsRelPrime p n ↔ ¬p ∣ n

See also Irreducible.coprime_iff_not_dvd.

theorem Irreducible.dvd_or_isRelPrime {α : Type u_1} [Monoid α] {p : α} {n : α} (hp : Irreducible p) : p ∣ n ∨ IsRelPrime p n

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 αˣ] : Associated = Eq

theorem prime_dvd_prime_iff_eq {M : Type u_5} [CancelCommMonoidWithZero M] [Unique Mˣ] {p : M} {q : M} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ p = q

theorem eq_of_prime_pow_eq {R : Type u_5} [CancelCommMonoidWithZero R] [Unique Rˣ] {p₁ : R} {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} [CancelCommMonoidWithZero R] [Unique Rˣ] {p₁ : R} {p₂ : R} {k₁ : ℕ} {k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) : p₁ = p₂

@[reducible, inline]

abbrev Associates (α : Type u_5) [Monoid α] : Type u_5

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

• Associates α = Quotient (Associated.setoid α)

@[reducible, inline]

abbrev Associates.mk {α : Type u_5} [Monoid α] (a : α) : Associates α

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

Equations

• Associates.mk a = ⟦a⟧

instance Associates.instInhabited {α : Type u_1} [Monoid α] : Inhabited (Associates α)

Equations

• Associates.instInhabited = { default := ⟦1⟧ }

theorem Associates.mk_eq_mk_iff_associated {α : Type u_1} [Monoid α] {a : α} {b : α} : Associates.mk a = Associates.mk b ↔ Associated a b

theorem Associates.quotient_mk_eq_mk {α : Type u_1} [Monoid α] (a : α) : ⟦a⟧ = Associates.mk a

theorem Associates.quot_mk_eq_mk {α : Type u_1} [Monoid α] (a : α) : Quot.mk Setoid.r a = Associates.mk a

@[simp]

theorem Associates.quot_out {α : Type u_1} [Monoid α] (a : Associates α) : Associates.mk (Quot.out a) = a

theorem Associates.mk_quot_out {α : Type u_1} [Monoid α] (a : α) : Associated (Quot.out (Associates.mk a)) a

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

theorem Associates.mk_surjective {α : Type u_1} [Monoid α] : Function.Surjective Associates.mk

instance Associates.instOne {α : Type u_1} [Monoid α] : One (Associates α)

Equations

• Associates.instOne = { one := ⟦1⟧ }

@[simp]

theorem Associates.mk_one {α : Type u_1} [Monoid α] : Associates.mk 1 = 1

theorem Associates.one_eq_mk_one {α : Type u_1} [Monoid α] : 1 = Associates.mk 1

@[simp]

theorem Associates.mk_eq_one {α : Type u_1} [Monoid α] {a : α} : Associates.mk a = 1 ↔ IsUnit a

instance Associates.instBot {α : Type u_1} [Monoid α] : Bot (Associates α)

Equations

• Associates.instBot = { bot := 1 }

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

instance Associates.instUniqueOfSubsingleton {α : Type u_1} [Monoid α] [Subsingleton α] : Unique (Associates α)

Equations

• Associates.instUniqueOfSubsingleton = { default := 1, uniq := ⋯ }

theorem Associates.mk_injective {α : Type u_1} [Monoid α] [Unique αˣ] : Function.Injective Associates.mk

instance Associates.instMul {α : Type u_1} [CommMonoid α] : Mul (Associates α)

Equations

• Associates.instMul = { mul := Quotient.map₂ (fun (x1 x2 : α) => x1 * x2) ⋯ }

theorem Associates.mk_mul_mk {α : Type u_1} [CommMonoid α] {x : α} {y : α} : Associates.mk x * Associates.mk y = Associates.mk (x * y)

instance Associates.instCommMonoid {α : Type u_1} [CommMonoid α] : CommMonoid (Associates α)

Equations

• Associates.instCommMonoid = CommMonoid.mk ⋯

instance Associates.instPreorder {α : Type u_1} [CommMonoid α] : Preorder (Associates α)

Equations

• Associates.instPreorder = Preorder.mk ⋯ ⋯ ⋯

def Associates.mkMonoidHom {α : Type u_1} [CommMonoid α] : α →* Associates α

Associates.mk as a MonoidHom.

Equations

• Associates.mkMonoidHom = { toFun := Associates.mk, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Associates.mkMonoidHom_apply {α : Type u_1} [CommMonoid α] (a : α) : Associates.mkMonoidHom a = Associates.mk a

theorem Associates.associated_map_mk {α : Type u_1} [CommMonoid α] {f : Associates α →* α} (hinv : Function.RightInverse (⇑f) Associates.mk) (a : α) : Associated a (f (Associates.mk a))

theorem Associates.mk_pow {α : Type u_1} [CommMonoid α] (a : α) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n

theorem Associates.dvd_eq_le {α : Type u_1} [CommMonoid α] : (fun (x1 x2 : Associates α) => x1 ∣ x2) = fun (x1 x2 : Associates α) => x1 ≤ x2

instance Associates.uniqueUnits {α : Type u_1} [CommMonoid α] : Unique (Associates α)ˣ

Equations

• Associates.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

@[deprecated mul_eq_one]

theorem Associates.mul_eq_one_iff {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} : a * b = 1 ↔ a = 1 ∧ b = 1

Alias of mul_eq_one.

@[deprecated Subsingleton.elim]

theorem Associates.units_eq_one {α : Sort u} [h : Subsingleton α] (a : α) (b : α) : a = b

Alias of Subsingleton.elim.

@[simp]

theorem Associates.coe_unit_eq_one {α : Type u_1} [CommMonoid α] (u : (Associates α)ˣ) : ↑u = 1

theorem Associates.isUnit_iff_eq_one {α : Type u_1} [CommMonoid α] (a : Associates α) : IsUnit a ↔ a = 1

theorem Associates.isUnit_iff_eq_bot {α : Type u_1} [CommMonoid α] {a : Associates α} : IsUnit a ↔ a = ⊥

theorem Associates.isUnit_mk {α : Type u_1} [CommMonoid α] {a : α} : IsUnit (Associates.mk a) ↔ IsUnit a

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

theorem Associates.one_le {α : Type u_1} [CommMonoid α] {a : Associates α} : 1 ≤ a

theorem Associates.le_mul_right {α : Type u_1} [CommMonoid α] {a : Associates α} {b : Associates α} : a ≤ a * b

theorem Associates.le_mul_left {α : Type u_1} [CommMonoid α] {a : Associates α} {b : Associates α} : a ≤ b * a

instance Associates.instOrderBot {α : Type u_1} [CommMonoid α] : OrderBot (Associates α)

Equations

• Associates.instOrderBot = OrderBot.mk ⋯

@[simp]

theorem Associates.mk_dvd_mk {α : Type u_1} [CommMonoid α] {a : α} {b : α} : Associates.mk a ∣ Associates.mk b ↔ a ∣ b

theorem Associates.dvd_of_mk_le_mk {α : Type u_1} [CommMonoid α] {a : α} {b : α} : Associates.mk a ≤ Associates.mk b → a ∣ b

theorem Associates.mk_le_mk_of_dvd {α : Type u_1} [CommMonoid α] {a : α} {b : α} : a ∣ b → Associates.mk a ≤ Associates.mk b

theorem Associates.mk_le_mk_iff_dvd {α : Type u_1} [CommMonoid α] {a : α} {b : α} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b

@[deprecated Associates.mk_le_mk_iff_dvd]

theorem Associates.mk_le_mk_iff_dvd_iff {α : Type u_1} [CommMonoid α] {a : α} {b : α} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b

Alias of Associates.mk_le_mk_iff_dvd.

@[simp]

theorem Associates.isPrimal_mk {α : Type u_1} [CommMonoid α] {a : α} : IsPrimal (Associates.mk a) ↔ IsPrimal a

@[deprecated Associates.isPrimal_mk]

theorem Associates.isPrimal_iff {α : Type u_1} [CommMonoid α] {a : α} : IsPrimal (Associates.mk a) ↔ IsPrimal a

Alias of Associates.isPrimal_mk.

@[simp]

theorem Associates.decompositionMonoid_iff {α : Type u_1} [CommMonoid α] : DecompositionMonoid (Associates α) ↔ DecompositionMonoid α

instance Associates.instDecompositionMonoid {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] : DecompositionMonoid (Associates α)

Equations

• ⋯ = ⋯

@[simp]

theorem Associates.mk_isRelPrime_iff {α : Type u_1} [CommMonoid α] {a : α} {b : α} : IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

instance Associates.instZero {α : Type u_1} [Zero α] [Monoid α] : Zero (Associates α)

Equations

• Associates.instZero = { zero := ⟦0⟧ }

instance Associates.instTopOfZero {α : Type u_1} [Zero α] [Monoid α] : Top (Associates α)

Equations

• Associates.instTopOfZero = { top := 0 }

@[simp]

theorem Associates.mk_zero {α : Type u_1} [Zero α] [Monoid α] : Associates.mk 0 = 0

@[simp]

theorem Associates.mk_eq_zero {α : Type u_1} [MonoidWithZero α] {a : α} : Associates.mk a = 0 ↔ a = 0

@[simp]

theorem Associates.quot_out_zero {α : Type u_1} [MonoidWithZero α] : Quot.out 0 = 0

theorem Associates.mk_ne_zero {α : Type u_1} [MonoidWithZero α] {a : α} : Associates.mk a ≠ 0 ↔ a ≠ 0

instance Associates.instNontrivial {α : Type u_1} [MonoidWithZero α] [Nontrivial α] : Nontrivial (Associates α)

Equations

• ⋯ = ⋯

theorem Associates.exists_non_zero_rep {α : Type u_1} [MonoidWithZero α] {a : Associates α} : a ≠ 0 → ∃ (a0 : α), a0 ≠ 0 ∧ Associates.mk a0 = a

instance Associates.instCommMonoidWithZero {α : Type u_1} [CommMonoidWithZero α] : CommMonoidWithZero (Associates α)

Equations

• Associates.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance Associates.instOrderTop {α : Type u_1} [CommMonoidWithZero α] : OrderTop (Associates α)

Equations

• Associates.instOrderTop = OrderTop.mk ⋯

@[simp]

theorem Associates.le_zero {α : Type u_1} [CommMonoidWithZero α] (a : Associates α) : a ≤ 0

instance Associates.instBoundedOrder {α : Type u_1} [CommMonoidWithZero α] : BoundedOrder (Associates α)

Equations

• Associates.instBoundedOrder = BoundedOrder.mk

instance Associates.instDecidableRelDvd {α : Type u_1} [CommMonoidWithZero α] [DecidableRel fun (x1 x2 : α) => x1 ∣ x2] : DecidableRel fun (x1 x2 : Associates α) => x1 ∣ x2

Equations

• a.instDecidableRelDvd b = Quotient.recOnSubsingleton₂ a b fun (x x_1 : α) => decidable_of_iff' (x ∣ x_1) ⋯

theorem Associates.Prime.le_or_le {α : Type u_1} [CommMonoidWithZero α] {p : Associates α} (hp : Prime p) {a : Associates α} {b : Associates α} (h : p ≤ a * b) : p ≤ a ∨ p ≤ b

@[simp]

theorem Associates.prime_mk {α : Type u_1} [CommMonoidWithZero α] {p : α} : Prime (Associates.mk p) ↔ Prime p

@[simp]

theorem Associates.irreducible_mk {α : Type u_1} [CommMonoidWithZero α] {a : α} : Irreducible (Associates.mk a) ↔ Irreducible a

@[simp]

theorem Associates.mk_dvdNotUnit_mk_iff {α : Type u_1} [CommMonoidWithZero α] {a : α} {b : α} : DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

theorem Associates.dvdNotUnit_of_lt {α : Type u_1} [CommMonoidWithZero α] {a : Associates α} {b : Associates α} (hlt : a < b) : DvdNotUnit a b

theorem Associates.irreducible_iff_prime_iff {α : Type u_1} [CommMonoidWithZero α] : (∀ (a : α), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates α), Irreducible a ↔ Prime a

instance Associates.instPartialOrder {α : Type u_1} [CancelCommMonoidWithZero α] : PartialOrder (Associates α)

Equations

• Associates.instPartialOrder = PartialOrder.mk ⋯

instance Associates.instCancelCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] : CancelCommMonoidWithZero (Associates α)

Equations

• Associates.instCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk

theorem associates_irreducible_iff_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecompositionMonoid α] {p : Associates α} : Irreducible p ↔ Prime p

instance Associates.instNoZeroDivisors {α : Type u_1} [CancelCommMonoidWithZero α] : NoZeroDivisors (Associates α)

Equations

• ⋯ = ⋯

theorem Associates.le_of_mul_le_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] (a : Associates α) (b : Associates α) (c : Associates α) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c

theorem Associates.one_or_eq_of_le_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {m : Associates α} (hp : Prime p) (hle : m ≤ p) : m = 1 ∨ m = p

theorem Associates.dvdNotUnit_iff_lt {α : Type u_1} [CancelCommMonoidWithZero α] {a : Associates α} {b : Associates α} : DvdNotUnit a b ↔ a < b

theorem Associates.le_one_iff {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} : p ≤ 1 ↔ p = 1

theorem DvdNotUnit.isUnit_of_irreducible_right {α : Type u_1} [CommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) (hq : Irreducible q) : IsUnit p

theorem not_irreducible_of_not_unit_dvdNotUnit {α : Type u_1} [CommMonoidWithZero α] {p : α} {q : α} (hp : ¬IsUnit p) (h : DvdNotUnit p q) : ¬Irreducible q

theorem DvdNotUnit.not_unit {α : Type u_1} [CommMonoidWithZero α] {p : α} {q : α} (hp : DvdNotUnit p q) : ¬IsUnit q

theorem dvdNotUnit_of_dvdNotUnit_associated {α : Type u_1} [CommMonoidWithZero α] [Nontrivial α] {p : α} {q : α} {r : α} (h : DvdNotUnit p q) (h' : Associated q r) : DvdNotUnit p r

theorem isUnit_of_associated_mul {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {b : α} (h : Associated (p * b) p) (hp : p ≠ 0) : IsUnit b

theorem DvdNotUnit.not_associated {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) : ¬Associated p q

theorem DvdNotUnit.ne {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) : p ≠ q

theorem pow_injective_of_not_unit {α : Type u_1} [CancelCommMonoidWithZero α] {q : α} (hq : ¬IsUnit q) (hq' : q ≠ 0) : Function.Injective fun (n : ℕ) => q ^ n

theorem dvd_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} {q : α} (hp : Prime p) (n : ℕ) : q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ Associated q (p ^ i)