Associated, prime, and irreducible elements.
theorem
prime.div_or_div
{α : Type u_1}
[comm_monoid_with_zero α]
{p : α}
(hp : prime p)
{a b : α} :
theorem
prime.dvd_of_dvd_pow
{α : Type u_1}
[comm_monoid_with_zero α]
{p : α}
(hp : prime p)
{a : α}
{n : ℕ} :
theorem
exists_mem_multiset_dvd_of_prime
{α : Type u_1}
[comm_monoid_with_zero α]
{s : multiset α}
{p : α} :
@[class]
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.
Instances
theorem
irreducible.is_unit_or_is_unit
{α : Type u_1}
[monoid α]
{p : α}
(hp : irreducible p)
{a b : α} :
theorem
of_irreducible_mul
{α : Type u_1}
[monoid α]
{x y : α} :
irreducible (x * y) → is_unit x ∨ is_unit y
theorem
irreducible_of_prime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{p : α} :
prime p → irreducible p
theorem
dvd_symm_of_irreducible
{α : Type u_1}
[monoid α]
{p q : α} :
irreducible p → irreducible q → p ∣ q → q ∣ p
If p and q are irreducible, then p ∣ q implies q ∣ p.
theorem
dvd_symm_iff_of_irreducible
{α : Type u_1}
[monoid α]
{p q : α} :
irreducible p → irreducible q → (p ∣ q ↔ q ∣ p)
Two elements of a monoid are associated if one of them is another one
multiplied by a unit on the right.
theorem
associated.trans
{α : Type u_1}
[monoid α]
{x y z : α} :
associated x y → associated y z → associated x z
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 := _}
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 : α) :
a * b = 1 → associated a 1
theorem
associated_one_of_associated_mul_one
{α : Type u_1}
[comm_monoid α]
{a b : α} :
associated (a * b) 1 → associated a 1
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_of_dvd_dvd
{α : Type u_1}
[cancel_monoid_with_zero α]
{a b : α} :
a ∣ b → b ∣ a → associated a b
theorem
dvd_dvd_iff_associated
{α : Type u_1}
[cancel_monoid_with_zero α]
{a b : α} :
a ∣ b ∧ b ∣ a ↔ associated a b
theorem
exists_associated_mem_of_dvd_prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{p : α}
(hp : prime p)
{s : multiset α} :
theorem
dvd_iff_dvd_of_rel_left
{α : Type u_1}
[comm_monoid_with_zero α]
{a b c : α} :
associated a b → (a ∣ c ↔ b ∣ c)
theorem
dvd_iff_dvd_of_rel_right
{α : Type u_1}
[comm_semiring α]
{a b c : α} :
associated b c → (a ∣ b ↔ a ∣ c)
theorem
eq_zero_iff_of_associated
{α : Type u_1}
[comm_semiring α]
{a b : α} :
associated a b → (a = 0 ↔ b = 0)
theorem
ne_zero_iff_of_associated
{α : Type u_1}
[comm_semiring α]
{a b : α} :
associated a b → (a ≠ 0 ↔ b ≠ 0)
theorem
prime_of_associated
{α : Type u_1}
[comm_semiring α]
{p q : α} :
associated p q → prime p → prime q
theorem
prime_iff_of_associated
{α : Type u_1}
[comm_semiring α]
{p q : α} :
associated p q → (prime p ↔ prime q)
theorem
is_unit_iff_of_associated
{α : Type u_1}
[monoid α]
{a b : α} :
associated a b → (is_unit a ↔ is_unit b)
theorem
irreducible_of_associated
{α : Type u_1}
[comm_semiring α]
{p q : α} :
associated p q → irreducible p → irreducible q
theorem
irreducible_iff_of_associated
{α : Type u_1}
[comm_semiring α]
{p q : α} :
associated p q → (irreducible p ↔ irreducible q)
theorem
associated_mul_left_cancel
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{a b c d : α} :
associated (a * b) (c * d) → associated a c → a ≠ 0 → associated b d
theorem
associated_mul_right_cancel
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{a b c d : α} :
associated (a * b) (c * d) → associated b d → b ≠ 0 → associated a c
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. associates α
forms a monoid.
Equations
- associates α = quotient (associated.setoid α)
The canonical quotient map from a monoid α into the associates of α
Equations
- associates.mk a = ⟦a⟧
@[instance]
theorem
associates.mk_eq_mk_iff_associated
{α : Type u_1}
[monoid α]
{a b : α} :
associates.mk a = associates.mk b ↔ associated a b
theorem
associates.quot_mk_eq_mk
{α : Type u_1}
[monoid α]
(a : α) :
quot.mk setoid.r a = associates.mk a
theorem
associates.forall_associated
{α : Type u_1}
[monoid α]
{p : associates α → Prop} :
(∀ (a : associates α), p a) ↔ ∀ (a : α), p (associates.mk a)
@[instance]
@[instance]
Equations
- associates.has_bot = {bot := 1}
@[instance]
Equations
- associates.has_mul = {mul := λ (a' b' : associates α), quotient.lift_on₂ a' b' (λ (a b : α), ⟦a * b⟧) associates.has_mul._proof_1}
theorem
associates.mk_mul_mk
{α : Type u_1}
[comm_monoid α]
{x y : α} :
associates.mk x * associates.mk y = associates.mk (x * y)
@[instance]
Equations
- associates.comm_monoid = {mul := has_mul.mul associates.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
@[instance]
Equations
- associates.preorder = {le := has_dvd.dvd monoid_has_dvd, lt := λ (a b : associates α), a ∣ b ∧ ¬b ∣ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
theorem
associates.mk_pow
{α : Type u_1}
[comm_monoid α]
(a : α)
(n : ℕ) :
associates.mk (a ^ n) = associates.mk a ^ n
theorem
associates.rel_associated_iff_map_eq_map
{α : Type u_1}
[comm_monoid α]
{p q : multiset α} :
@[instance]
Equations
- associates.unique_units = {to_inhabited := {default := 1}, uniq := _}
theorem
associates.is_unit_mk
{α : Type u_1}
[comm_monoid α]
{a : α} :
is_unit (associates.mk a) ↔ is_unit a
@[instance]
@[instance]
Equations
- associates.has_top = {top := 0}
@[simp]
theorem
associates.mk_eq_zero
{α : Type u_1}
[comm_monoid_with_zero α]
{a : α} :
associates.mk a = 0 ↔ a = 0
@[instance]
Equations
- associates.comm_monoid_with_zero = {mul := comm_monoid.mul associates.comm_monoid, mul_assoc := _, one := comm_monoid.one associates.comm_monoid, one_mul := _, mul_one := _, mul_comm := _, zero := 0, zero_mul := _, mul_zero := _}
@[instance]
def
associates.nontrivial
{α : Type u_1}
[comm_monoid_with_zero α]
[nontrivial α] :
nontrivial (associates α)
Equations
theorem
associates.dvd_of_mk_le_mk
{α : Type u_1}
[comm_monoid_with_zero α]
{a b : α} :
associates.mk a ≤ associates.mk b → a ∣ b
theorem
associates.mk_le_mk_of_dvd
{α : Type u_1}
[comm_monoid_with_zero α]
{a b : α} :
a ∣ b → associates.mk a ≤ associates.mk b
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
theorem
associates.prime.le_or_le
{α : Type u_1}
[comm_monoid_with_zero α]
{p : associates α}
(hp : p.prime)
{a b : associates α} :
theorem
associates.exists_mem_multiset_le_of_prime
{α : Type u_1}
[comm_monoid_with_zero α]
{s : multiset (associates α)}
{p : associates α} :
theorem
associates.prime_mk
{α : Type u_1}
[comm_monoid_with_zero α]
(p : α) :
(associates.mk p).prime ↔ prime p
@[instance]
Equations
- associates.partial_order = {le := preorder.le associates.preorder, lt := preorder.lt associates.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[instance]
def
associates.order_bot
{α : Type u_1}
[comm_cancel_monoid_with_zero α] :
order_bot (associates α)
Equations
- associates.order_bot = {bot := 1, le := partial_order.le associates.partial_order, lt := partial_order.lt associates.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
def
associates.order_top
{α : Type u_1}
[comm_cancel_monoid_with_zero α] :
order_top (associates α)
Equations
- associates.order_top = {top := 0, le := partial_order.le associates.partial_order, lt := partial_order.lt associates.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
Equations
theorem
associates.prod_eq_zero_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
{s : multiset (associates α)} :
theorem
associates.irreducible_mk_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a : α) :
irreducible (associates.mk a) ↔ irreducible a
theorem
associates.eq_of_mul_eq_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a b c : associates α) :
theorem
associates.le_of_mul_le_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a b c : associates α) :
theorem
associates.one_or_eq_of_le_of_prime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(p m : associates α) :