# 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} (p : α) :

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
Instances For
theorem Prime.ne_zero {α : Type u_1} {p : α} (hp : ) :
p 0
theorem Prime.not_unit {α : Type u_1} {p : α} (hp : ) :
theorem Prime.not_dvd_one {α : Type u_1} {p : α} (hp : ) :
¬p 1
theorem Prime.ne_one {α : Type u_1} {p : α} (hp : ) :
p 1
theorem Prime.dvd_or_dvd {α : Type u_1} {p : α} (hp : ) {a : α} {b : α} (h : p a * b) :
p a p b
theorem Prime.dvd_mul {α : Type u_1} {p : α} (hp : ) {a : α} {b : α} :
p a * b p a p b
theorem Prime.isPrimal {α : Type u_1} {p : α} (hp : ) :
theorem Prime.not_dvd_mul {α : Type u_1} {p : α} (hp : ) {a : α} {b : α} (ha : ¬p a) (hb : ¬p b) :
¬p a * b
theorem Prime.dvd_of_dvd_pow {α : Type u_1} {p : α} (hp : ) {a : α} {n : } (h : p a ^ n) :
p a
theorem Prime.dvd_pow_iff_dvd {α : Type u_1} {p : α} (hp : ) {a : α} {n : } (hn : n 0) :
p a ^ n p a
@[simp]
theorem not_prime_zero {α : Type u_1} :
@[simp]
theorem not_prime_one {α : Type u_1} :
theorem comap_prime {α : Type u_1} {β : Type u_2} {F : Type u_5} {G : Type u_6} [FunLike F α β] [] [FunLike G β α] [MulHomClass G β α] (f : F) (g : G) {p : α} (hinv : ∀ (a : α), g (f a) = a) (hp : Prime (f p)) :
theorem MulEquiv.prime_iff {α : Type u_1} {β : Type u_2} {p : α} (e : α ≃* β) :
Prime (e p)
theorem Prime.left_dvd_or_dvd_right_of_dvd_mul {α : Type u_1} {p : α} (hp : ) {a : α} {b : α} :
a p * bp a a b
theorem Prime.pow_dvd_of_dvd_mul_left {α : Type u_1} {p : α} {a : α} {b : α} (hp : ) (n : ) (h : ¬p a) (h' : p ^ n a * b) :
p ^ n b
theorem Prime.pow_dvd_of_dvd_mul_right {α : Type u_1} {p : α} {a : α} {b : α} (hp : ) (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} {p : α} {a : α} {b : α} {n : } (hp : ) (hpow : p ^ n.succ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 b) :
p a
theorem prime_pow_succ_dvd_mul {α : Type u_5} {p : α} {x : α} {y : α} (h : ) {i : } (hxy : p ^ (i + 1) x * y) :
p ^ (i + 1) x p y
structure Irreducible {α : Type u_1} [] (p : α) :

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

p is not a unit

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

if p factors then one factor is a unit

Instances For
theorem Irreducible.not_unit {α : Type u_1} [] {p : α} (self : ) :

p is not a unit

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

if p factors then one factor is a unit

theorem Irreducible.not_dvd_one {α : Type u_1} [] {p : α} (hp : ) :
¬p 1
theorem Irreducible.isUnit_or_isUnit {α : Type u_1} [] {p : α} (hp : ) {a : α} {b : α} (h : p = a * b) :
theorem irreducible_iff {α : Type u_1} [] {p : α} :
¬ ∀ (a b : α), p = a * b
@[simp]
theorem not_irreducible_one {α : Type u_1} [] :
theorem Irreducible.ne_one {α : Type u_1} [] {p : α} :
p 1
@[simp]
theorem not_irreducible_zero {α : Type u_1} [] :
theorem Irreducible.ne_zero {α : Type u_1} [] {p : α} :
p 0
theorem of_irreducible_mul {α : Type u_5} [] {x : α} {y : α} :
Irreducible (x * y)
theorem not_irreducible_pow {α : Type u_5} [] {x : α} {n : } (hn : n 1) :
theorem irreducible_or_factor {α : Type u_5} [] (x : α) (h : ¬) :
∃ (a : α), ∃ (b : α), ¬ ¬ a * b = x
theorem Irreducible.dvd_symm {α : Type u_1} [] {p : α} {q : α} (hp : ) (hq : ) :
p qq p

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

theorem Irreducible.dvd_comm {α : Type u_1} [] {p : α} {q : α} (hp : ) (hq : ) :
p q q p
theorem irreducible_units_mul {α : Type u_1} [] (a : αˣ) (b : α) :
Irreducible (a * b)
theorem irreducible_isUnit_mul {α : Type u_1} [] {a : α} {b : α} (h : ) :
theorem irreducible_mul_units {α : Type u_1} [] (a : αˣ) (b : α) :
Irreducible (b * a)
theorem irreducible_mul_isUnit {α : Type u_1} [] {a : α} {b : α} (h : ) :
theorem irreducible_mul_iff {α : Type u_1} [] {a : α} {b : α} :
theorem Irreducible.not_square {α : Type u_1} [] {a : α} (ha : ) :
theorem IsSquare.not_irreducible {α : Type u_1} [] {a : α} (ha : ) :
theorem Irreducible.prime_of_isPrimal {α : Type u_1} {a : α} (irr : ) (primal : ) :
theorem Irreducible.prime {α : Type u_1} {a : α} (irr : ) :
theorem Prime.irreducible {α : Type u_1} {p : α} (hp : ) :
theorem irreducible_iff_prime {α : Type u_1} {a : α} :
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} {p : α} (hp : ) {a : α} {b : α} {k : } {l : } :
p ^ k ap ^ l bp ^ (k + l + 1) a * bp ^ (k + 1) a p ^ (l + 1) b
theorem Prime.not_square {α : Type u_1} {p : α} (hp : ) :
theorem IsSquare.not_prime {α : Type u_1} {a : α} (ha : ) :
theorem not_prime_pow {α : Type u_1} {a : α} {n : } (hn : n 1) :
¬Prime (a ^ n)
def Associated {α : Type u_1} [] (x : α) (y : α) :

Two elements of a Monoid are Associated if one of them is another one multiplied by a unit on the right.

Equations
• = ∃ (u : αˣ), x * u = y
Instances For
theorem Associated.refl {α : Type u_1} [] (x : α) :
theorem Associated.rfl {α : Type u_1} [] {x : α} :
instance Associated.instIsRefl {α : Type u_1} [] :
IsRefl α Associated
Equations
• =
theorem Associated.symm {α : Type u_1} [] {x : α} {y : α} :
instance Associated.instIsSymm {α : Type u_1} [] :
IsSymm α Associated
Equations
• =
theorem Associated.comm {α : Type u_1} [] {x : α} {y : α} :
theorem Associated.trans {α : Type u_1} [] {x : α} {y : α} {z : α} :
instance Associated.instIsTrans {α : Type u_1} [] :
IsTrans α Associated
Equations
• =
def Associated.setoid (α : Type u_5) [] :

The setoid of the relation x ~ᵤ y iff there is a unit u such that x * u = y

Equations
• = { r := Associated, iseqv := }
Instances For
theorem Associated.map {M : Type u_5} {N : Type u_6} [] [] {F : Type u_7} [FunLike F M N] [] (f : F) {x : M} {y : M} (ha : ) :
Associated (f x) (f y)
theorem unit_associated_one {α : Type u_1} [] {u : αˣ} :
Associated (↑u) 1
@[simp]
theorem associated_one_iff_isUnit {α : Type u_1} [] {a : α} :
@[simp]
theorem associated_zero_iff_eq_zero {α : Type u_1} [] (a : α) :
a = 0
theorem associated_one_of_mul_eq_one {α : Type u_1} [] {a : α} (b : α) (hab : a * b = 1) :
theorem associated_one_of_associated_mul_one {α : Type u_1} [] {a : α} {b : α} :
Associated (a * b) 1
theorem associated_mul_unit_left {β : Type u_5} [] (a : β) (u : β) (hu : ) :
Associated (a * u) a
theorem associated_unit_mul_left {β : Type u_5} [] (a : β) (u : β) (hu : ) :
Associated (u * a) a
theorem associated_mul_unit_right {β : Type u_5} [] (a : β) (u : β) (hu : ) :
Associated a (a * u)
theorem associated_unit_mul_right {β : Type u_5} [] (a : β) (u : β) (hu : ) :
Associated a (u * a)
theorem associated_mul_isUnit_left_iff {β : Type u_5} [] {a : β} {u : β} {b : β} (hu : ) :
Associated (a * u) b
theorem associated_isUnit_mul_left_iff {β : Type u_5} [] {u : β} {a : β} {b : β} (hu : ) :
Associated (u * a) b
theorem associated_mul_isUnit_right_iff {β : Type u_5} [] {a : β} {b : β} {u : β} (hu : ) :
Associated a (b * u)
theorem associated_isUnit_mul_right_iff {β : Type u_5} [] {a : β} {u : β} {b : β} (hu : ) :
Associated a (u * b)
@[simp]
theorem associated_mul_unit_left_iff {β : Type u_5} [] {a : β} {b : β} {u : βˣ} :
Associated (a * u) b
@[simp]
theorem associated_unit_mul_left_iff {β : Type u_5} [] {a : β} {b : β} {u : βˣ} :
Associated (u * a) b
@[simp]
theorem associated_mul_unit_right_iff {β : Type u_5} [] {a : β} {b : β} {u : βˣ} :
Associated a (b * u)
@[simp]
theorem associated_unit_mul_right_iff {β : Type u_5} [] {a : β} {b : β} {u : βˣ} :
Associated a (u * b)
theorem Associated.mul_left {α : Type u_1} [] (a : α) {b : α} {c : α} (h : ) :
Associated (a * b) (a * c)
theorem Associated.mul_right {α : Type u_1} [] {a : α} {b : α} (h : ) (c : α) :
Associated (a * c) (b * c)
theorem Associated.mul_mul {α : Type u_1} [] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : Associated a₁ b₁) (h₂ : Associated a₂ b₂) :
Associated (a₁ * a₂) (b₁ * b₂)
theorem Associated.pow_pow {α : Type u_1} [] {a : α} {b : α} {n : } (h : ) :
Associated (a ^ n) (b ^ n)
theorem Associated.dvd {α : Type u_1} [] {a : α} {b : α} :
a b
theorem Associated.dvd' {α : Type u_1} [] {a : α} {b : α} (h : ) :
b a
theorem Associated.dvd_dvd {α : Type u_1} [] {a : α} {b : α} (h : ) :
a b b a
theorem associated_of_dvd_dvd {α : Type u_1} {a : α} {b : α} (hab : a b) (hba : b a) :
theorem dvd_dvd_iff_associated {α : Type u_1} {a : α} {b : α} :
a b b a
instance instDecidableRelAssociatedOfDvd {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : α) => Associated x x_1
Equations
theorem Associated.dvd_iff_dvd_left {α : Type u_1} [] {a : α} {b : α} {c : α} (h : ) :
a c b c
theorem Associated.dvd_iff_dvd_right {α : Type u_1} [] {a : α} {b : α} {c : α} (h : ) :
a b a c
theorem Associated.eq_zero_iff {α : Type u_1} [] {a : α} {b : α} (h : ) :
a = 0 b = 0
theorem Associated.ne_zero_iff {α : Type u_1} [] {a : α} {b : α} (h : ) :
a 0 b 0
theorem Associated.neg_left {α : Type u_1} [] [] {a : α} {b : α} (h : ) :
theorem Associated.neg_right {α : Type u_1} [] [] {a : α} {b : α} (h : ) :
theorem Associated.neg_neg {α : Type u_1} [] [] {a : α} {b : α} (h : ) :
Associated (-a) (-b)
theorem Associated.prime {α : Type u_1} {p : α} {q : α} (h : ) (hp : ) :
theorem prime_mul_iff {α : Type u_1} {x : α} {y : α} :
Prime (x * y)
@[simp]
theorem prime_pow_iff {α : Type u_1} {p : α} {n : } :
Prime (p ^ n) n = 1
theorem Irreducible.dvd_iff {α : Type u_1} [] {x : α} {y : α} (hx : ) :
y x
theorem Irreducible.associated_of_dvd {α : Type u_1} [] {p : α} {q : α} (p_irr : ) (q_irr : ) (dvd : p q) :
theorem Irreducible.dvd_irreducible_iff_associated {α : Type u_1} [] {p : α} {q : α} (pp : ) (qp : ) :
p q
theorem Prime.associated_of_dvd {α : Type u_1} {p : α} {q : α} (p_prime : ) (q_prime : ) (dvd : p q) :
theorem Prime.dvd_prime_iff_associated {α : Type u_1} {p : α} {q : α} (pp : ) (qp : ) :
p q
theorem Associated.prime_iff {α : Type u_1} {p : α} {q : α} (h : ) :
theorem Associated.isUnit {α : Type u_1} [] {a : α} {b : α} (h : ) :
theorem Associated.isUnit_iff {α : Type u_1} [] {a : α} {b : α} (h : ) :
theorem Irreducible.isUnit_iff_not_associated_of_dvd {α : Type u_1} [] {x : α} {y : α} (hx : ) (hy : y x) :
theorem Associated.irreducible {α : Type u_1} [] {p : α} {q : α} (h : ) (hp : ) :
theorem Associated.irreducible_iff {α : Type u_1} [] {p : α} {q : α} (h : ) :
theorem Associated.of_mul_left {α : Type u_1} {a : α} {b : α} {c : α} {d : α} (h : Associated (a * b) (c * d)) (h₁ : ) (ha : a 0) :
theorem Associated.of_mul_right {α : Type u_1} {a : α} {b : α} {c : α} {d : α} :
Associated (a * b) (c * d)b 0
theorem Associated.of_pow_associated_of_prime {α : Type u_1} {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} {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} [] {p : α} {n : α} (hp : ) :
¬p n

See also Irreducible.coprime_iff_not_dvd.

theorem Irreducible.dvd_or_isRelPrime {α : Type u_1} [] {p : α} {n : α} (hp : ) :
p n
theorem associated_iff_eq {α : Type u_1} [] [] {x : α} {y : α} :
x = y
theorem associated_eq_eq {α : Type u_1} [] [] :
Associated = Eq
theorem prime_dvd_prime_iff_eq {M : Type u_5} [] {p : M} {q : M} (pp : ) (qp : ) :
p q p = q
theorem eq_of_prime_pow_eq {R : Type u_5} [] {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} [] {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) [] :
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
Instances For
@[reducible, inline]
abbrev Associates.mk {α : Type u_5} [] (a : α) :

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

Equations
• = a
Instances For
instance Associates.instInhabited {α : Type u_1} [] :
Equations
• Associates.instInhabited = { default := 1 }
theorem Associates.mk_eq_mk_iff_associated {α : Type u_1} [] {a : α} {b : α} :
theorem Associates.quotient_mk_eq_mk {α : Type u_1} [] (a : α) :
a =
theorem Associates.quot_mk_eq_mk {α : Type u_1} [] (a : α) :
Quot.mk Setoid.r a =
@[simp]
theorem Associates.quot_out {α : Type u_1} [] (a : ) :
= a
theorem Associates.mk_quot_out {α : Type u_1} [] (a : α) :
theorem Associates.forall_associated {α : Type u_1} [] {p : } :
(∀ (a : ), p a) ∀ (a : α), p
theorem Associates.mk_surjective {α : Type u_1} [] :
Function.Surjective Associates.mk
instance Associates.instOne {α : Type u_1} [] :
Equations
• Associates.instOne = { one := 1 }
@[simp]
theorem Associates.mk_one {α : Type u_1} [] :
theorem Associates.one_eq_mk_one {α : Type u_1} [] :
@[simp]
theorem Associates.mk_eq_one {α : Type u_1} [] {a : α} :
instance Associates.instBot {α : Type u_1} [] :
Equations
• Associates.instBot = { bot := 1 }
theorem Associates.bot_eq_one {α : Type u_1} [] :
= 1
theorem Associates.exists_rep {α : Type u_1} [] (a : ) :
∃ (a0 : α), = a
Equations
• Associates.instUniqueOfSubsingleton = { default := 1, uniq := }
theorem Associates.mk_injective {α : Type u_1} [] [] :
Function.Injective Associates.mk
instance Associates.instMul {α : Type u_1} [] :
Equations
theorem Associates.mk_mul_mk {α : Type u_1} [] {x : α} {y : α} :
instance Associates.instCommMonoid {α : Type u_1} [] :
Equations
• Associates.instCommMonoid =
instance Associates.instPreorder {α : Type u_1} [] :
Equations
def Associates.mkMonoidHom {α : Type u_1} [] :
α →*

Associates.mk as a MonoidHom.

Equations
• Associates.mkMonoidHom = { toFun := Associates.mk, map_one' := , map_mul' := }
Instances For
@[simp]
theorem Associates.mkMonoidHom_apply {α : Type u_1} [] (a : α) :
Associates.mkMonoidHom a =
theorem Associates.associated_map_mk {α : Type u_1} [] {f : →* α} (hinv : Function.RightInverse (⇑f) Associates.mk) (a : α) :
Associated a (f )
theorem Associates.mk_pow {α : Type u_1} [] (a : α) (n : ) :
theorem Associates.dvd_eq_le {α : Type u_1} [] :
(fun (x x_1 : ) => x x_1) = fun (x x_1 : ) => x x_1
theorem Associates.mul_eq_one_iff {α : Type u_1} [] {x : } {y : } :
x * y = 1 x = 1 y = 1
theorem Associates.units_eq_one {α : Type u_1} [] (u : (Associates α)ˣ) :
u = 1
instance Associates.uniqueUnits {α : Type u_1} [] :
Equations
• Associates.uniqueUnits = { default := 1, uniq := }
@[simp]
theorem Associates.coe_unit_eq_one {α : Type u_1} [] (u : (Associates α)ˣ) :
u = 1
theorem Associates.isUnit_iff_eq_one {α : Type u_1} [] (a : ) :
a = 1
theorem Associates.isUnit_iff_eq_bot {α : Type u_1} [] {a : } :
a =
theorem Associates.isUnit_mk {α : Type u_1} [] {a : α} :
theorem Associates.mul_mono {α : Type u_1} [] {a : } {b : } {c : } {d : } (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem Associates.one_le {α : Type u_1} [] {a : } :
1 a
theorem Associates.le_mul_right {α : Type u_1} [] {a : } {b : } :
a a * b
theorem Associates.le_mul_left {α : Type u_1} [] {a : } {b : } :
a b * a
instance Associates.instOrderBot {α : Type u_1} [] :
Equations
• Associates.instOrderBot =
@[simp]
theorem Associates.mk_dvd_mk {α : Type u_1} [] {a : α} {b : α} :
a b
theorem Associates.dvd_of_mk_le_mk {α : Type u_1} [] {a : α} {b : α} :
a b
theorem Associates.mk_le_mk_of_dvd {α : Type u_1} [] {a : α} {b : α} :
a b
theorem Associates.mk_le_mk_iff_dvd {α : Type u_1} [] {a : α} {b : α} :
a b
@[deprecated Associates.mk_le_mk_iff_dvd]
theorem Associates.mk_le_mk_iff_dvd_iff {α : Type u_1} [] {a : α} {b : α} :
a b

Alias of Associates.mk_le_mk_iff_dvd.

@[simp]
theorem Associates.isPrimal_mk {α : Type u_1} [] {a : α} :
@[deprecated Associates.isPrimal_mk]
theorem Associates.isPrimal_iff {α : Type u_1} [] {a : α} :

Alias of Associates.isPrimal_mk.

@[simp]
instance Associates.instDecompositionMonoid {α : Type u_1} [] :
Equations
• =
@[simp]
theorem Associates.mk_isRelPrime_iff {α : Type u_1} [] {a : α} {b : α} :
instance Associates.instZero {α : Type u_1} [Zero α] [] :
Equations
• Associates.instZero = { zero := 0 }
instance Associates.instTopOfZero {α : Type u_1} [Zero α] [] :
Equations
• Associates.instTopOfZero = { top := 0 }
@[simp]
theorem Associates.mk_zero {α : Type u_1} [Zero α] [] :
@[simp]
theorem Associates.mk_eq_zero {α : Type u_1} [] {a : α} :
a = 0
@[simp]
theorem Associates.quot_out_zero {α : Type u_1} [] :
= 0
theorem Associates.mk_ne_zero {α : Type u_1} [] {a : α} :
a 0
instance Associates.instNontrivial {α : Type u_1} [] [] :
Equations
• =
theorem Associates.exists_non_zero_rep {α : Type u_1} [] {a : } :
a 0∃ (a0 : α), a0 0 = a
Equations
• Associates.instCommMonoidWithZero =
instance Associates.instOrderTop {α : Type u_1} :
Equations
• Associates.instOrderTop =
@[simp]
theorem Associates.le_zero {α : Type u_1} (a : ) :
a 0
instance Associates.instBoundedOrder {α : Type u_1} :
Equations
• Associates.instBoundedOrder = BoundedOrder.mk
instance Associates.instDecidableRelDvd {α : Type u_1} [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : ) => x x_1
Equations
theorem Associates.Prime.le_or_le {α : Type u_1} {p : } (hp : ) {a : } {b : } (h : p a * b) :
p a p b
@[simp]
theorem Associates.prime_mk {α : Type u_1} {p : α} :
@[simp]
theorem Associates.irreducible_mk {α : Type u_1} {a : α} :
@[simp]
theorem Associates.mk_dvdNotUnit_mk_iff {α : Type u_1} {a : α} {b : α} :
theorem Associates.dvdNotUnit_of_lt {α : Type u_1} {a : } {b : } (hlt : a < b) :
theorem Associates.irreducible_iff_prime_iff {α : Type u_1} :
(∀ (a : α), ) ∀ (a : ),
instance Associates.instPartialOrder {α : Type u_1} :
Equations
• Associates.instPartialOrder =
Equations
• Associates.instCancelCommMonoidWithZero = let __src := inferInstance; CancelCommMonoidWithZero.mk
theorem associates_irreducible_iff_prime {α : Type u_1} {p : } :
instance Associates.instNoZeroDivisors {α : Type u_1} :
Equations
• =
theorem Associates.le_of_mul_le_mul_left {α : Type u_1} (a : ) (b : ) (c : ) (ha : a 0) :
a * b a * cb c
theorem Associates.one_or_eq_of_le_of_prime {α : Type u_1} {p : } {m : } (hp : ) (hle : m p) :
m = 1 m = p
theorem Associates.dvdNotUnit_iff_lt {α : Type u_1} {a : } {b : } :
a < b
theorem Associates.le_one_iff {α : Type u_1} {p : } :
p 1 p = 1
theorem DvdNotUnit.isUnit_of_irreducible_right {α : Type u_1} {p : α} {q : α} (h : ) (hq : ) :
theorem not_irreducible_of_not_unit_dvdNotUnit {α : Type u_1} {p : α} {q : α} (hp : ¬) (h : ) :
theorem DvdNotUnit.not_unit {α : Type u_1} {p : α} {q : α} (hp : ) :
theorem dvdNotUnit_of_dvdNotUnit_associated {α : Type u_1} [] {p : α} {q : α} {r : α} (h : ) (h' : ) :
theorem isUnit_of_associated_mul {α : Type u_1} {p : α} {b : α} (h : Associated (p * b) p) (hp : p 0) :
theorem DvdNotUnit.not_associated {α : Type u_1} {p : α} {q : α} (h : ) :
theorem DvdNotUnit.ne {α : Type u_1} {p : α} {q : α} (h : ) :
p q
theorem pow_injective_of_not_unit {α : Type u_1} {q : α} (hq : ¬) (hq' : q 0) :
Function.Injective fun (n : ) => q ^ n
theorem dvd_prime_pow {α : Type u_1} {p : α} {q : α} (hp : ) (n : ) :
q p ^ n ∃ (i : ), i n Associated q (p ^ i)