Documentation

Mathlib.Algebra.Associated

Associated, prime, and irreducible elements. #

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

prime element of a CommMonoidWithZero

Equations
theorem Prime.ne_zero {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) :
p 0
theorem Prime.not_unit {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) :
theorem Prime.not_dvd_one {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) :
¬p 1
theorem Prime.ne_one {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) :
p 1
theorem Prime.dvd_or_dvd {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} (h : p a * b) :
p a p b
theorem Prime.dvd_of_dvd_pow {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {n : } (h : p a ^ n) :
p a
@[simp]
theorem not_prime_zero {α : Type u_1} [inst : CommMonoidWithZero α] :
@[simp]
theorem not_prime_one {α : Type u_1} [inst : CommMonoidWithZero α] :
theorem comap_prime {α : Type u_1} {β : Type u_3} [inst : CommMonoidWithZero α] [inst : CommMonoidWithZero β] {F : Type u_2} {G : Type u_4} [inst : MonoidWithZeroHomClass F α β] [inst : 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} [inst : CommMonoidWithZero α] [inst : CommMonoidWithZero β] {p : α} (e : α ≃* β) :
Prime p Prime (e p)
theorem Prime.left_dvd_or_dvd_right_of_dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {a : α} {b : α} :
a p * bp a a b
theorem Prime.pow_dvd_of_dvd_mul_left {α : Type u_1} [inst : 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} [inst : 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} [inst : CancelCommMonoidWithZero α] {p : α} {a : α} {b : α} {n : } (hp : Prime p) (hpow : p ^ Nat.succ n a ^ Nat.succ n * b ^ n) (hb : ¬p ^ 2 b) :
p a
theorem prime_pow_succ_dvd_mul {α : Type u_1} [inst : 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} [inst : Monoid α] (p : α) :
  • p is not a unit

    not_unit : ¬IsUnit p
  • if p factors then one factor is a unit

    isUnit_or_isUnit' : ∀ (a b : α), p = a * bIsUnit a IsUnit 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.

Instances For
    theorem Irreducible.not_dvd_one {α : Type u_1} [inst : CommMonoid α] {p : α} (hp : Irreducible p) :
    ¬p 1
    theorem Irreducible.isUnit_or_isUnit {α : Type u_1} [inst : Monoid α] {p : α} (hp : Irreducible p) {a : α} {b : α} (h : p = a * b) :
    theorem irreducible_iff {α : Type u_1} [inst : Monoid α] {p : α} :
    Irreducible p ¬IsUnit p ∀ (a b : α), p = a * bIsUnit a IsUnit b
    @[simp]
    theorem not_irreducible_one {α : Type u_1} [inst : Monoid α] :
    theorem Irreducible.ne_one {α : Type u_1} [inst : Monoid α] {p : α} :
    Irreducible pp 1
    @[simp]
    theorem not_irreducible_zero {α : Type u_1} [inst : MonoidWithZero α] :
    theorem Irreducible.ne_zero {α : Type u_1} [inst : MonoidWithZero α] {p : α} :
    Irreducible pp 0
    theorem of_irreducible_mul {α : Type u_1} [inst : Monoid α] {x : α} {y : α} :
    Irreducible (x * y)IsUnit x IsUnit y
    theorem of_irreducible_pow {α : Type u_1} [inst : Monoid α] {x : α} {n : } (hn : n 1) :
    Irreducible (x ^ n)IsUnit x
    theorem irreducible_or_factor {α : Type u_1} [inst : Monoid α] (x : α) (h : ¬IsUnit x) :
    Irreducible x a b, ¬IsUnit a ¬IsUnit b a * b = x
    theorem Irreducible.dvd_symm {α : Type u_1} [inst : Monoid α] {p : α} {q : α} (hp : Irreducible p) (hq : Irreducible q) :
    p qq p

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

    theorem Irreducible.dvd_comm {α : Type u_1} [inst : Monoid α] {p : α} {q : α} (hp : Irreducible p) (hq : Irreducible q) :
    p q q p
    theorem irreducible_units_mul {α : Type u_1} [inst : Monoid α] (a : αˣ) (b : α) :
    theorem irreducible_isUnit_mul {α : Type u_1} [inst : Monoid α] {a : α} {b : α} (h : IsUnit a) :
    theorem irreducible_mul_units {α : Type u_1} [inst : Monoid α] (a : αˣ) (b : α) :
    theorem irreducible_mul_isUnit {α : Type u_1} [inst : Monoid α] {a : α} {b : α} (h : IsUnit a) :
    theorem irreducible_mul_iff {α : Type u_1} [inst : Monoid α] {a : α} {b : α} :
    theorem Irreducible.not_square {α : Type u_1} [inst : CommMonoid α] {a : α} (ha : Irreducible a) :
    theorem IsSquare.not_irreducible {α : Type u_1} [inst : CommMonoid α] {a : α} (ha : IsSquare a) :
    theorem Prime.irreducible {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} (hp : Prime p) :
    theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {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} [inst : CancelCommMonoidWithZero α] {p : α} (hp : Prime p) :
    theorem IsSquare.not_prime {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a : α} (ha : IsSquare a) :
    theorem pow_not_prime {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a : α} {n : } (hn : n 1) :
    ¬Prime (a ^ n)
    def Associated {α : Type u_1} [inst : Monoid α] (x : α) (y : α) :

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

    Equations
    theorem Associated.refl {α : Type u_1} [inst : Monoid α] (x : α) :
    theorem Associated.symm {α : Type u_1} [inst : Monoid α] {x : α} {y : α} :
    theorem Associated.comm {α : Type u_1} [inst : Monoid α] {x : α} {y : α} :
    theorem Associated.trans {α : Type u_1} [inst : Monoid α] {x : α} {y : α} {z : α} :
    Associated x yAssociated y zAssociated x z
    def Associated.setoid (α : Type u_1) [inst : 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} [inst : Monoid α] {u : αˣ} :
    Associated (u) 1
    theorem associated_one_iff_isUnit {α : Type u_1} [inst : Monoid α] {a : α} :
    theorem associated_zero_iff_eq_zero {α : Type u_1} [inst : MonoidWithZero α] (a : α) :
    Associated a 0 a = 0
    theorem associated_one_of_mul_eq_one {α : Type u_1} [inst : CommMonoid α] {a : α} (b : α) (hab : a * b = 1) :
    theorem associated_one_of_associated_mul_one {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
    Associated (a * b) 1Associated a 1
    theorem associated_mul_unit_left {β : Type u_1} [inst : Monoid β] (a : β) (u : β) (hu : IsUnit u) :
    Associated (a * u) a
    theorem associated_unit_mul_left {β : Type u_1} [inst : CommMonoid β] (a : β) (u : β) (hu : IsUnit u) :
    Associated (u * a) a
    theorem associated_mul_unit_right {β : Type u_1} [inst : Monoid β] (a : β) (u : β) (hu : IsUnit u) :
    Associated a (a * u)
    theorem associated_unit_mul_right {β : Type u_1} [inst : CommMonoid β] (a : β) (u : β) (hu : IsUnit u) :
    Associated a (u * a)
    theorem associated_mul_isUnit_left_iff {β : Type u_1} [inst : Monoid β] {a : β} {u : β} {b : β} (hu : IsUnit u) :
    theorem associated_isUnit_mul_left_iff {β : Type u_1} [inst : CommMonoid β] {u : β} {a : β} {b : β} (hu : IsUnit u) :
    theorem associated_mul_isUnit_right_iff {β : Type u_1} [inst : Monoid β] {a : β} {b : β} {u : β} (hu : IsUnit u) :
    theorem associated_isUnit_mul_right_iff {β : Type u_1} [inst : CommMonoid β] {a : β} {u : β} {b : β} (hu : IsUnit u) :
    @[simp]
    theorem associated_mul_unit_left_iff {β : Type u_1} [inst : Monoid β] {a : β} {b : β} {u : βˣ} :
    Associated (a * u) b Associated a b
    @[simp]
    theorem associated_unit_mul_left_iff {β : Type u_1} [inst : CommMonoid β] {a : β} {b : β} {u : βˣ} :
    Associated (u * a) b Associated a b
    @[simp]
    theorem associated_mul_unit_right_iff {β : Type u_1} [inst : Monoid β] {a : β} {b : β} {u : βˣ} :
    Associated a (b * u) Associated a b
    @[simp]
    theorem associated_unit_mul_right_iff {β : Type u_1} [inst : CommMonoid β] {a : β} {b : β} {u : βˣ} :
    Associated a (u * b) Associated a b
    theorem Associated.mul_mul {α : Type u_1} [inst : CommMonoid α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
    Associated a₁ b₁Associated a₂ b₂Associated (a₁ * a₂) (b₁ * b₂)
    theorem Associated.mul_left {α : Type u_1} [inst : CommMonoid α] (a : α) {b : α} {c : α} (h : Associated b c) :
    Associated (a * b) (a * c)
    theorem Associated.mul_right {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} (h : Associated a b) (c : α) :
    Associated (a * c) (b * c)
    theorem Associated.pow_pow {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} {n : } (h : Associated a b) :
    Associated (a ^ n) (b ^ n)
    theorem Associated.dvd {α : Type u_1} [inst : Monoid α] {a : α} {b : α} :
    Associated a ba b
    theorem Associated.dvd_dvd {α : Type u_1} [inst : Monoid α] {a : α} {b : α} (h : Associated a b) :
    a b b a
    theorem associated_of_dvd_dvd {α : Type u_1} [inst : CancelMonoidWithZero α] {a : α} {b : α} (hab : a b) (hba : b a) :
    theorem dvd_dvd_iff_associated {α : Type u_1} [inst : CancelMonoidWithZero α] {a : α} {b : α} :
    a b b a Associated a b
    theorem Associated.dvd_iff_dvd_left {α : Type u_1} [inst : Monoid α] {a : α} {b : α} {c : α} (h : Associated a b) :
    a c b c
    theorem Associated.dvd_iff_dvd_right {α : Type u_1} [inst : Monoid α] {a : α} {b : α} {c : α} (h : Associated b c) :
    a b a c
    theorem Associated.eq_zero_iff {α : Type u_1} [inst : MonoidWithZero α] {a : α} {b : α} (h : Associated a b) :
    a = 0 b = 0
    theorem Associated.ne_zero_iff {α : Type u_1} [inst : MonoidWithZero α] {a : α} {b : α} (h : Associated a b) :
    a 0 b 0
    theorem Associated.prime {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} {q : α} (h : Associated p q) (hp : Prime p) :
    theorem Irreducible.associated_of_dvd {α : Type u_1} [inst : CancelMonoidWithZero α] {p : α} {q : α} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p q) :
    theorem Irreducible.dvd_irreducible_iff_associated {α : Type u_1} [inst : CancelMonoidWithZero α] {p : α} {q : α} (pp : Irreducible p) (qp : Irreducible q) :
    theorem Prime.associated_of_dvd {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {q : α} (p_prime : Prime p) (q_prime : Prime q) (dvd : p q) :
    theorem Prime.dvd_prime_iff_associated {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {q : α} (pp : Prime p) (qp : Prime q) :
    theorem Associated.prime_iff {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} {q : α} (h : Associated p q) :
    theorem Associated.isUnit {α : Type u_1} [inst : Monoid α] {a : α} {b : α} (h : Associated a b) :
    IsUnit aIsUnit b
    theorem Associated.isUnit_iff {α : Type u_1} [inst : Monoid α] {a : α} {b : α} (h : Associated a b) :
    theorem Associated.irreducible {α : Type u_1} [inst : Monoid α] {p : α} {q : α} (h : Associated p q) (hp : Irreducible p) :
    theorem Associated.irreducible_iff {α : Type u_1} [inst : Monoid α] {p : α} {q : α} (h : Associated p q) :
    theorem Associated.of_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] {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} [inst : CancelCommMonoidWithZero α] {a : α} {b : α} {c : α} {d : α} :
    Associated (a * b) (c * d)Associated b db 0Associated a c
    theorem Associated.of_pow_associated_of_prime {α : Type u_1} [inst : 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} [inst : CancelCommMonoidWithZero α] {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} [inst : Monoid α] [inst : Unique αˣ] (u : αˣ) :
    u = 1
    theorem associated_iff_eq {α : Type u_1} [inst : Monoid α] [inst : Unique αˣ] {x : α} {y : α} :
    Associated x y x = y
    theorem associated_eq_eq {α : Type u_1} [inst : Monoid α] [inst : Unique αˣ] :
    Associated = Eq
    theorem prime_dvd_prime_iff_eq {M : Type u_1} [inst : CancelCommMonoidWithZero M] [inst : 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_1} [inst : CancelCommMonoidWithZero R] [inst : 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_1} [inst : CancelCommMonoidWithZero R] [inst : Unique Rˣ] {p₁ : R} {p₂ : R} {k₁ : } {k₂ : } (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
    p₁ = p₂
    @[inline]
    abbrev Associates (α : Type u_1) [inst : 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
    @[inline]
    abbrev Associates.mk {α : Type u_1} [inst : Monoid α] (a : α) :

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

    Equations
    instance Associates.instInhabitedAssociates {α : Type u_1} [inst : Monoid α] :
    Equations
    theorem Associates.mk_eq_mk_iff_associated {α : Type u_1} [inst : Monoid α] {a : α} {b : α} :
    theorem Associates.quot_mk_eq_mk {α : Type u_1} [inst : Monoid α] (a : α) :
    Quot.mk Setoid.r a = Associates.mk a
    theorem Associates.forall_associated {α : Type u_1} [inst : Monoid α] {p : Associates αProp} :
    ((a : Associates α) → p a) (a : α) → p (Associates.mk a)
    theorem Associates.mk_surjective {α : Type u_1} [inst : Monoid α] :
    Function.Surjective Associates.mk
    instance Associates.instOneAssociates {α : Type u_1} [inst : Monoid α] :
    Equations
    @[simp]
    theorem Associates.mk_one {α : Type u_1} [inst : Monoid α] :
    theorem Associates.one_eq_mk_one {α : Type u_1} [inst : Monoid α] :
    instance Associates.instBotAssociates {α : Type u_1} [inst : Monoid α] :
    Equations
    • Associates.instBotAssociates = { bot := 1 }
    theorem Associates.bot_eq_one {α : Type u_1} [inst : Monoid α] :
    = 1
    theorem Associates.exists_rep {α : Type u_1} [inst : Monoid α] (a : Associates α) :
    a0, Associates.mk a0 = a
    instance Associates.instUniqueAssociates {α : Type u_1} [inst : Monoid α] [inst : Subsingleton α] :
    Equations
    • Associates.instUniqueAssociates = { toInhabited := { default := 1 }, uniq := (_ : ∀ (a : Associates α), a = default) }
    theorem Associates.mk_injective {α : Type u_1} [inst : Monoid α] [inst : Unique αˣ] :
    Function.Injective Associates.mk
    instance Associates.instMulAssociatesToMonoid {α : Type u_1} [inst : CommMonoid α] :
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Associates.mk_mul_mk {α : Type u_1} [inst : CommMonoid α] {x : α} {y : α} :
    Equations
    Equations
    def Associates.mkMonoidHom {α : Type u_1} [inst : CommMonoid α] :

    Associates.mk as a MonoidHom.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Associates.mkMonoidHom_apply {α : Type u_1} [inst : CommMonoid α] (a : α) :
    Associates.mkMonoidHom a = Associates.mk a
    theorem Associates.associated_map_mk {α : Type u_1} [inst : CommMonoid α] {f : Associates α →* α} (hinv : Function.RightInverse (f) Associates.mk) (a : α) :
    theorem Associates.mk_pow {α : Type u_1} [inst : CommMonoid α] (a : α) (n : ) :
    theorem Associates.dvd_eq_le {α : Type u_1} [inst : CommMonoid α] :
    (fun x x_1 => x x_1) = fun x x_1 => x x_1
    theorem Associates.mul_eq_one_iff {α : Type u_1} [inst : CommMonoid α] {x : Associates α} {y : Associates α} :
    x * y = 1 x = 1 y = 1
    theorem Associates.units_eq_one {α : Type u_1} [inst : CommMonoid α] (u : (Associates α)ˣ) :
    u = 1
    instance Associates.uniqueUnits {α : Type u_1} [inst : CommMonoid α] :
    Equations
    • Associates.uniqueUnits = { toInhabited := { default := 1 }, uniq := (_ : ∀ (u : (Associates α)ˣ), u = 1) }
    theorem Associates.coe_unit_eq_one {α : Type u_1} [inst : CommMonoid α] (u : (Associates α)ˣ) :
    u = 1
    theorem Associates.isUnit_iff_eq_one {α : Type u_1} [inst : CommMonoid α] (a : Associates α) :
    IsUnit a a = 1
    theorem Associates.isUnit_iff_eq_bot {α : Type u_1} [inst : CommMonoid α] {a : Associates α} :
    theorem Associates.isUnit_mk {α : Type u_1} [inst : CommMonoid α] {a : α} :
    theorem Associates.mul_mono {α : Type u_1} [inst : 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} [inst : CommMonoid α] {a : Associates α} :
    1 a
    theorem Associates.le_mul_right {α : Type u_1} [inst : CommMonoid α] {a : Associates α} {b : Associates α} :
    a a * b
    theorem Associates.le_mul_left {α : Type u_1} [inst : CommMonoid α] {a : Associates α} {b : Associates α} :
    a b * a
    Equations
    • Associates.instOrderBotAssociatesToMonoidToLEInstPreorderAssociatesToMonoid = OrderBot.mk (_ : ∀ (x : Associates α), 1 x)
    theorem Associates.dvd_of_mk_le_mk {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
    theorem Associates.mk_le_mk_of_dvd {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
    theorem Associates.mk_le_mk_iff_dvd_iff {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
    theorem Associates.mk_dvd_mk {α : Type u_1} [inst : CommMonoid α] {a : α} {b : α} :
    instance Associates.instZeroAssociates {α : Type u_1} [inst : Zero α] [inst : Monoid α] :
    Equations
    instance Associates.instTopAssociates {α : Type u_1} [inst : Zero α] [inst : Monoid α] :
    Equations
    • Associates.instTopAssociates = { top := 0 }
    @[simp]
    theorem Associates.mk_eq_zero {α : Type u_1} [inst : MonoidWithZero α] {a : α} :
    theorem Associates.mk_ne_zero {α : Type u_1} [inst : MonoidWithZero α] {a : α} :
    theorem Associates.exists_non_zero_rep {α : Type u_1} [inst : MonoidWithZero α] {a : Associates α} :
    a 0a0, a0 0 Associates.mk a0 = a
    Equations
    Equations
    • Associates.instOrderTopAssociatesToMonoidToMonoidWithZeroToLEInstPreorderAssociatesToMonoidToCommMonoid = OrderTop.mk (_ : ∀ (a : Associates α), c, = a * c)
    Equations
    • Associates.instBoundedOrderAssociatesToMonoidToMonoidWithZeroToLEInstPreorderAssociatesToMonoidToCommMonoid = BoundedOrder.mk
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Associates.Prime.le_or_le {α : Type u_1} [inst : CommMonoidWithZero α] {p : Associates α} (hp : Prime p) {a : Associates α} {b : Associates α} (h : p a * b) :
    p a p b
    theorem Associates.prime_mk {α : Type u_1} [inst : CommMonoidWithZero α] (p : α) :
    theorem Associates.dvdNotUnit_of_lt {α : Type u_1} [inst : CommMonoidWithZero α] {a : Associates α} {b : Associates α} (hlt : a < b) :
    theorem Associates.irreducible_iff_prime_iff {α : Type u_1} [inst : CommMonoidWithZero α] :
    (∀ (a : α), Irreducible a Prime a) ∀ (a : Associates α), Irreducible a Prime a
    Equations
    • Associates.instPartialOrderAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = PartialOrder.mk (_ : ∀ (a' b' : Associates α), a' b'b' a'a' = b')
    Equations
    Equations
    • Associates.instCancelCommMonoidWithZeroAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = let src := inferInstance; CancelCommMonoidWithZero.mk
    theorem Associates.le_of_mul_le_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] (a : Associates α) (b : Associates α) (c : Associates α) (ha : a 0) :
    a * b a * cb c
    theorem Associates.one_or_eq_of_le_of_prime {α : Type u_1} [inst : CancelCommMonoidWithZero α] (p : Associates α) (m : Associates α) :
    Prime pm pm = 1 m = p
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Associates.le_one_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : Associates α} :
    p 1 p = 1
    theorem DvdNotUnit.isUnit_of_irreducible_right {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) (hq : Irreducible q) :
    theorem not_irreducible_of_not_unit_dvdNotUnit {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} {q : α} (hp : ¬IsUnit p) (h : DvdNotUnit p q) :
    theorem DvdNotUnit.not_unit {α : Type u_1} [inst : CommMonoidWithZero α] {p : α} {q : α} (hp : DvdNotUnit p q) :
    theorem dvdNotUnit_of_dvdNotUnit_associated {α : Type u_1} [inst : CommMonoidWithZero α] [inst : Nontrivial α] {p : α} {q : α} {r : α} (h : DvdNotUnit p q) (h' : Associated q r) :
    theorem isUnit_of_associated_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {b : α} (h : Associated (p * b) p) (hp : p 0) :
    theorem DvdNotUnit.not_associated {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) :
    theorem DvdNotUnit.ne {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {q : α} (h : DvdNotUnit p q) :
    p q
    theorem pow_injective_of_not_unit {α : Type u_1} [inst : CancelCommMonoidWithZero α] {q : α} (hq : ¬IsUnit q) (hq' : q 0) :
    Function.Injective fun n => q ^ n
    theorem dvd_prime_pow {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α} {q : α} (hp : Prime p) (n : ) :
    q p ^ n i, i n Associated q (p ^ i)