Prime.irreducible
theorem Prime.irreducible : ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {p : α}, Prime p → Irreducible p := by
sorry
This theorem states that for any type `α` which is a `CancelCommMonoidWithZero` (a commutative monoid with zero that has the cancellation property), if an element `p` of `α` is a prime element, then it is also an irreducible element. In mathematical terms, given a prime element `p` in a commutative monoid with zero, then `p` is irreducible. This means, `p` cannot be expressed as the product of two non-unit elements.
More concisely: In a commutative monoid with zero having cancellation property, every prime element is irreducible.
|
Associated.of_mul_left
theorem Associated.of_mul_left :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a b c d : α},
Associated (a * b) (c * d) → Associated a c → a ≠ 0 → Associated b d
This theorem states that for any type `α` that has an instance of the `CancelCommMonoidWithZero` typeclass, and for any four elements `a`, `b`, `c`, `d` of this type, if the elements `a * b` and `c * d` are associated and the elements `a` and `c` are associated, and if `a` is not zero, then the elements `b` and `d` are also associated. In mathematical terms, if `a * b` is associated with `c * d` and `a` is associated with `c`, with `a` being non-zero, then `b` is associated with `d`. The `Associated` relation here means that one element can be obtained by multiplying the other by a unit.
More concisely: If `a` is a non-zero element of a type `α` with `CancelCommMonoidWithZero`, and `a * b` is associative with `c * d` and `a` is associative with `c`, then `b` is associative with `d`.
|
associated_mul_unit_left
theorem associated_mul_unit_left : ∀ {β : Type u_5} [inst : Monoid β] (a u : β), IsUnit u → Associated (a * u) a := by
sorry
The theorem `associated_mul_unit_left` states that for any type `β` that forms a Monoid, for any elements `a` and `u` of that Monoid, if `u` is a unit (meaning it has a two-sided inverse), then `a * u` and `a` are associated. In the context of a Monoid, two elements are said to be associated if one of them can be obtained by multiplying the other one with a unit on the right.
More concisely: For any Monoid `β` and elements `a` and `u` in `β` with `u` being a unit, `a * u` is associated with `a`, i.e., there exists a unit `v` such that `a * u = a * (u * v)`.
|
Associates.mk_one
theorem Associates.mk_one : ∀ {α : Type u_1} [inst : Monoid α], Associates.mk 1 = 1
This theorem, `Associates.mk_one`, states that for any type `α` that forms a monoid, the canonical quotient map when applied to the identity element `1` in the monoid, results in the identity element `1` in the monoid of associates. In other words, it asserts that the image of the monoid identity under the canonical homomorphism to the associates is also the identity.
More concisely: For any monoid `α`, the image of its identity element `1` under the canonical homomorphism to the monoid of associates is the identity element `1` in the monoid of associates.
|
Associated.mul_left
theorem Associated.mul_left :
∀ {α : Type u_1} [inst : Monoid α] (a : α) {b c : α}, Associated b c → Associated (a * b) (a * c)
The `Associated.mul_left` theorem states that for any type `α` that forms a `Monoid`, given an element `a` of the `Monoid` and two other elements `b` and `c` such that `b` and `c` are `Associated`, the product of `a` and `b` is `Associated` with the product of `a` and `c`. In other words, in a `Monoid`, if two elements are `Associated`, meaning that one can be obtained by multiplying the other by a unit, then premultiplying both elements by the same factor preserves this `Associated` relationship.
More concisely: If `a` is a unit in a monoid `α`, and `b` and `c` are associated elements, then `a * b` is associated with `a * c`.
|
Prime.dvd_of_dvd_pow
theorem Prime.dvd_of_dvd_pow :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : α}, Prime p → ∀ {a : α} {n : ℕ}, p ∣ a ^ n → p ∣ a
The theorem `Prime.dvd_of_dvd_pow` states that for any type `α` that forms a commutative monoid with zero, any prime element `p` of this type and any element `a` of this type, if `p` divides `a` raised to the power of a natural number `n`, then `p` also divides `a`. In other words, if a prime number is a divisor of a power of another number, it must also be a divisor of that number itself.
More concisely: If a prime number `p` divides the power `a^n` of an element `a` in a commutative monoid with zero, then `p` divides `a`.
|
Associated.isUnit
theorem Associated.isUnit : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, Associated a b → IsUnit a → IsUnit b := by
sorry
The theorem `Associated.isUnit` states that for any type `α` that forms a `Monoid`, given any two elements `a` and `b` of this type, if `a` and `b` are `Associated` (i.e., `a` can be obtained by multiplying `b` by a unit on the right), and if `a` is a `Unit` (i.e., `a` has a two-sided inverse), then `b` is also a `Unit`. This essentially says that being a unit is a preserved property under the association relation in a monoid.
More concisely: If `a` and `b` are associated elements in a monoid `α` with `a` being a unit, then `b` is also a unit.
|
Prime.dvd_or_dvd
theorem Prime.dvd_or_dvd :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : α}, Prime p → ∀ {a b : α}, p ∣ a * b → p ∣ a ∨ p ∣ b
The theorem `Prime.dvd_or_dvd` states that for any type `α` which has a commutative monoid with zero structure, and for any element `p` of `α` that is prime, whenever `p` divides the product of any two elements `a` and `b` (denoted as `p ∣ a * b`), then `p` must divide `a` or `p` must divide `b` (denoted as `p ∣ a ∨ p ∣ b`). This is a key property of prime elements in a commutative monoid with zero, mirroring the familiar property of prime numbers in the integers.
More concisely: In a commutative monoid with zero, if a prime element p divides the product of two elements a and b, then p divides a or p divides b.
|
Mathlib.Algebra.Associated._auxLemma.5
theorem Mathlib.Algebra.Associated._auxLemma.5 : ∀ {α : Type u_1} [inst : MonoidWithZero α], Irreducible 0 = False := by
sorry
This theorem, from the Mathlib library in Algebra under Associated, states that zero cannot be classified as irreducible for any type `α` that forms a monoid with zero. In the context of algebra, an element is said to be irreducible if it cannot be factored into the product of two non-unit elements. According to this theorem, zero is not an irreducible element.
More concisely: In any monoid type with zero, zero is not an irreducible element.
|
Mathlib.Algebra.Associated._auxLemma.3
theorem Mathlib.Algebra.Associated._auxLemma.3 :
∀ {α : Type u_1} [inst : Monoid α] {p : α},
Irreducible p = (¬IsUnit p ∧ ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b)
This theorem, named `Mathlib.Algebra.Associated._auxLemma.3`, states that for any type `α` that forms a monoid and any element `p` of `α`, `p` is irreducible if and only if `p` is not a unit and for all elements `a` and `b` in `α`, if `p` equals the product of `a` and `b`, then either `a` or `b` must be a unit. In the context of algebra, a monoid is a set equipped with an associative binary operation and an identity element, a unit is an element that has a multiplicative inverse, and an irreducible element is a non-unit element that cannot be expressed as a product of two non-unit elements.
More concisely: For any monoid `α` and element `p` in `α` that is not a unit, `p` is irreducible if and only if for all `a` and `b` in `α` such that `p = a * b`, either `a` or `b` is a unit.
|
Associates.mk_surjective
theorem Associates.mk_surjective : ∀ {α : Type u_1} [inst : Monoid α], Function.Surjective Associates.mk
The theorem `Associates.mk_surjective` states that for any type `α` with a `Monoid` structure, the function `Associates.mk`, which maps an element of the monoid to its associate, is surjective. This means that for every element in the set of associates of `α`, there exists an element in the original monoid `α` such that when the `Associates.mk` function is applied to this element, it produces the given associate. In other words, every associate can be created from some element in the original monoid using the `Associates.mk` function.
More concisely: For any monoid `α`, the function `Associates.mk` maps every element of its associates to some element in `α`.
|
not_irreducible_pow
theorem not_irreducible_pow : ∀ {α : Type u_5} [inst : Monoid α] {x : α} {n : ℕ}, n ≠ 1 → ¬Irreducible (x ^ n) := by
sorry
This theorem states that for any type `α` that is a Monoid, and any `x` of type `α` and `n` of type `ℕ` (natural number), if `n` is not equal to 1, then `x ^ n` (i.e., `x` raised to the power of `n`) is not irreducible. In the context of algebra, an element of a monoid is said to be irreducible if it is not the unit and cannot be expressed as the product of two non-units.
More concisely: For any monoid `α` and `x ∈ α` (x being a non-unit), if `n ∈ ℕ` (natural number) is not equal to 1, then `x ^ n` is not irreducible.
|
Associates.quot_out
theorem Associates.quot_out : ∀ {α : Type u_1} [inst : Monoid α] (a : Associates α), Associates.mk (Quot.out a) = a
This theorem, `Associates.quot_out`, states that for any type `α` that has a monoid structure and any element `a` of the `Associates` of `α`, if we first take an element from the equivalence class of `a` using `Quot.out` and then map back to the `Associates` of `α` using `Associates.mk`, we get the original element `a` back. In other words, it verifies that the process of picking a representative from an equivalence class and then finding the equivalence class again will yield the original equivalence class. The theorem encapsulates the idea that the `Associates.mk` and `Quot.out` operations are inverse to each other up to the equivalence relation.
More concisely: For any type `α` with a monoid structure and any `a` in the associates of `α`, `Associates.mk (Quot.out a) = a` holds up to the associates equivalence relation.
|
Associates.isUnit_iff_eq_one
theorem Associates.isUnit_iff_eq_one : ∀ {α : Type u_1} [inst : CommMonoid α] (a : Associates α), IsUnit a ↔ a = 1 := by
sorry
The theorem `Associates.isUnit_iff_eq_one` states that for any commutative monoid `α`, and for any element `a` of the associates of `α`, `a` is a unit if and only if `a` is equal to 1. Here, the associates of a monoid `α` is the quotient of `α` by the `Associated` relation, which states that two elements are associated if there exists a unit that multiplied by one of them results in the other. A unit in a monoid `M` is an element that has a two-sided inverse.
More concisely: In a commutative monoid, an element is a unit if and only if it is equal to the identity element. Equivalently, elements are associates if and only if one is a unit and they are equal.
|
dvd_dvd_iff_associated
theorem dvd_dvd_iff_associated :
∀ {α : Type u_1} [inst : CancelMonoidWithZero α] {a b : α}, a ∣ b ∧ b ∣ a ↔ Associated a b
The theorem `dvd_dvd_iff_associated` states that for any type `α` that is a `CancelMonoidWithZero`, and any two elements `a` and `b` of that type, `a` divides `b` and `b` divides `a` if and only if `a` and `b` are associated. Here, two elements are called associated if one of them is equal to the other multiplied by a unit on the right, where a unit is an element that has a multiplicative inverse.
More concisely: For any type `α` that is a `CancelMonoidWithZero` and any elements `a` and `b` of `α`, `a` divides `b` and `b` divides `a` if and only if `a` and `b` are right associate with some unit in `α`.
|
Irreducible.isUnit_or_isUnit'
theorem Irreducible.isUnit_or_isUnit' :
∀ {α : Type u_1} [inst : Monoid α] {p : α}, Irreducible p → ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b
This theorem states that for any type `α` that has a `Monoid` structure, and for any element `p` of `α` which is irreducible, if `p` can be expressed as the product of two elements `a` and `b` (i.e., `p = a * b`), then one of these factors, `a` or `b`, must be a unit. In other words, if you can factor an irreducible element in a monoid, at least one of the factors must be a unit. A unit in this context is an element that has a two-sided inverse.
More concisely: In a monoid with an irreducible element `p`, if `p = a * b` for some elements `a` and `b`, then either `a` or `b` is a unit.
|
Associated.symm
theorem Associated.symm : ∀ {α : Type u_1} [inst : Monoid α] {x y : α}, Associated x y → Associated y x
The theorem `Associated.symm` states that for any given type `α` that forms a `Monoid`, if two elements `x` and `y` of `α` are `Associated` (meaning one of them is the other multiplied by a unit on the right), then the reverse is also true, i.e., `y` is `Associated` with `x`. In other words, the `Associated` relationship between `x` and `y` is symmetric.
More concisely: If `x` and `y` are associated elements in a monoid `α`, then `y` is associated with `x`.
|
Associated.mul_mul
theorem Associated.mul_mul :
∀ {α : Type u_1} [inst : CommMonoid α] {a₁ a₂ b₁ b₂ : α},
Associated a₁ b₁ → Associated a₂ b₂ → Associated (a₁ * a₂) (b₁ * b₂)
This theorem states that in a commutative monoid, if two elements `a₁` and `b₁` are associated, and another two elements `a₂` and `b₂` are also associated, then the products `a₁ * a₂` and `b₁ * b₂` are associated as well.
In general, two elements in a monoid are said to be associated if one can be obtained from the other by multiplying by a unit on the right. In this context, "associated" does not mean just "related" in some way, but has a specific mathematical meaning.
More concisely: In a commutative monoid, if elements `a₁` and `b₁`, and `a₂` and `b₂` are right-associated with some units `r₁` and `r₂` respectively, then `a₁ * a₂` and `b₁ * b₂` are associated, that is, there exists a unit `r` such that `a₁ * a₂ = b₁ * b₂ * r`.
|
Associated.dvd_iff_dvd_right
theorem Associated.dvd_iff_dvd_right :
∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, Associated b c → (a ∣ b ↔ a ∣ c)
This theorem states that, for any three elements `a`, `b`, and `c` in a `Monoid` structure, if `b` and `c` are `Associated` (meaning there exists a unit element such that `b` multiplied by this unit is `c`), then `a` divides `b` if and only if `a` divides `c`. In other words, the `Associated` relationship between `b` and `c` preserves the divisibility relationship with `a`. Here, division is defined in terms of the monoid operation.
More concisely: For any element `a` and associative elements `b` and `c` in a monoid, `a` divides `b` if and only if `a` divides `c` if and only if `b` is associated with `c` via some unit element.
|
Associates.mk_dvd_mk
theorem Associates.mk_dvd_mk :
∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, Associates.mk a ∣ Associates.mk b ↔ a ∣ b
The theorem `Associates.mk_dvd_mk` states that for any commutative monoid `α` and any elements `a` and `b` of `α`, the element `a` divides `b` if and only if the associate of `a` divides the associate of `b`. Here, the associate of an element from a monoid is obtained using the canonical quotient map, `Associates.mk`. In other words, the divisibility relationship between `a` and `b` is preserved when they are mapped into the associates of `α`.
More concisely: For all commutative monoids `α`, elements `a` and `b` in `α`, if `a` divides `b`, then the associates of `a` and `b` are related by the divisibility relation. (i.e., `Associates.mk a` divides `Associates.mk b`).
|
Associated.dvd_iff_dvd_left
theorem Associated.dvd_iff_dvd_left :
∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, Associated a b → (a ∣ c ↔ b ∣ c)
The theorem `Associated.dvd_iff_dvd_left` states that for any type `α` that forms a monoid, and any three elements `a`, `b`, and `c` of that monoid, if `a` and `b` are associated (which means there exists a unit `u` for which `a` times `u` equals `b`), then `a` divides `c` if and only if `b` divides `c`. In other words, if `a` and `b` are associated, then `a` and `b` have the same divisibility relation with `c`.
More concisely: For all monoids types `α` and elements `a, b, c` in `α`, if `a` is associated with `b` (i.e., `a = b * u` for some unit `u`), then `a` divides `c` if and only if `b` divides `c`.
|
Irreducible.not_unit
theorem Irreducible.not_unit : ∀ {α : Type u_1} [inst : Monoid α] {p : α}, Irreducible p → ¬IsUnit p
The theorem `Irreducible.not_unit` states that for any type `α` that forms a Monoid, if an element `p` of this Monoid is Irreducible, then `p` is not a unit. An irreducible element in a Monoid is one that cannot be expressed as a product of two non-unit elements, and a unit is an element that has a two-sided inverse. Hence, this theorem asserts the impossibility of an irreducible element also being a unit within a monoidal structure.
More concisely: In a Monoid, an Irreducible element is not a Unit.
|
associated_mul_isUnit_left_iff
theorem associated_mul_isUnit_left_iff :
∀ {β : Type u_5} [inst : Monoid β] {a u b : β}, IsUnit u → (Associated (a * u) b ↔ Associated a b)
This theorem states that for any type `β` that has a monoid structure, and for any elements `a`, `u`, and `b` of that type, if `u` is a unit (meaning it has a two-sided inverse in the monoid), then the statement "the element `a * u` is associated with b" is equivalent to the statement "the element `a` is associated with b". In other words, multiplication by a unit on the left does not change whether two elements are associated. In mathematical terms, two elements `x` and `y` of a monoid are said to be associated if there exists a unit `u` such that `x * u = y`.
More concisely: For any monoid `β` with unit `u`, if `a * u = b`, then `a` and `b` are associated. Conversely, if `a` and `b` are associated, then there exists a unit `u` such that `a * u = b`.
|
Associates.mk_le_mk_of_dvd
theorem Associates.mk_le_mk_of_dvd :
∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → Associates.mk a ≤ Associates.mk b
This theorem states that for any type `α` which is a commutative monoid, given any two elements `a` and `b` of this type, if `a` divides `b`, then the associate of `a` is less than or equal to the associate of `b`. Here, the associate of an element is simply the equivalence class of the element under the equivalence relation of being associated, which is defined by `Associates.mk`. This theorem essentially links the divisibility relation in the original monoid with the order relation in the associates.
More concisely: For any commutative monoid type `α` and elements `a, b` of `α`, if `a` divides `b`, then the associates of `a` and `b` are related by the ordering relation. (i.e., the associate of `a` is less than or equal to the associate of `b`).
|
associated_mul_unit_right
theorem associated_mul_unit_right : ∀ {β : Type u_5} [inst : Monoid β] (a u : β), IsUnit u → Associated a (a * u) := by
sorry
The theorem `associated_mul_unit_right` states that for any type `β` that has a `Monoid` structure, and for any elements `a` and `u` of `β`, if `u` is a unit (meaning it has a two-sided inverse), then `a` is `Associated` with `a * u`. In mathematical terms, this means there exists some unit `u` such that `a * u` equals to `a`, hence `a` is associated with `a * u`. This essentially says that the multiplication of any element by a unit doesn't change its association class in the monoid.
More concisely: For any monoid `β` and elements `a` and `u` in `β` with `u` being a unit, `a` is associated with `a * u`.
|
Associates.mk_mul_mk
theorem Associates.mk_mul_mk :
∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, Associates.mk x * Associates.mk y = Associates.mk (x * y) := by
sorry
This theorem, `Associates.mk_mul_mk`, states that for any type `α` that is a commutative monoid, and any two elements `x` and `y` of `α`, the product of the canonical quotient mappings of `x` and `y` into the `Associates` of `α` is equal to the canonical quotient mapping of the product of `x` and `y`. In other words, the function `Associates.mk` preserves the multiplication operation from the original monoid to the `Associates` structure.
More concisely: For any commutative monoid `α` and its elements `x` and `y`, the canonical quotient mappings of `x` and `y` into the `Associates` of `α` are equal to the canonical quotient mapping of the product of `x` and `y`.
|
Irreducible.dvd_iff
theorem Irreducible.dvd_iff :
∀ {α : Type u_1} [inst : Monoid α] {x y : α}, Irreducible x → (y ∣ x ↔ IsUnit y ∨ Associated x y)
The theorem `Irreducible.dvd_iff` states that for any type `α` that forms a `Monoid`, and any two elements `x` and `y` from `α`, if `x` is irreducible, then `y` divides `x` if and only if `y` is a unit, or `x` is associated with `y`. Here, `y` being a unit means that there exists an element which when multiplied with `y` gives the identity of the monoid. `x` is associated with `y` means that `x` can be represented as `y` multiplied by a unit.
More concisely: For any monoid `α` and irreducible elements `x` and `y` in `α`, `y` divides `x` if and only if `y` is a unit or `x` is associates with `y`.
|
associated_iff_eq
theorem associated_iff_eq : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Unique αˣ] {x y : α}, Associated x y ↔ x = y
The theorem `associated_iff_eq` states that for any type `α` that has a `Monoid` structure and a unique unit `αˣ`, and for any two elements `x` and `y` of type `α`, `x` and `y` are associated (i.e., one of them is the other one multiplied by a unit on the right) if and only if `x` equals `y`. This is, if there exists a unit `u` such that `x * u = y`, then `x` and `y` are equal.
More concisely: For any type `α` with a `Monoid` structure and unique unit `αˣ`, elements `x` and `y` are associates (i.e., there exists a unit `u` such that `x * u = y`) if and only if `x` is equal to `y`.
|
associated_of_dvd_dvd
theorem associated_of_dvd_dvd :
∀ {α : Type u_1} [inst : CancelMonoidWithZero α] {a b : α}, a ∣ b → b ∣ a → Associated a b
This theorem states that for any type `α` that forms a `CancelMonoidWithZero`, given any two elements `a` and `b` of this type, if `a` divides `b` and `b` divides `a`, then `a` and `b` are associated. In the context of monoids, two elements are considered associated if one can be obtained by multiplying the other by a unit on the right. In other words, `a` and `b` are associated if there exists a unit `u` such that `a * u = b`.
More concisely: If `α` is a type forming a `CancelMonoidWithZero` and `a` and `b` are elements of `α` such that `a` divides `b` and `b` divides `a`, then there exists a unit `u` such that `a * u = b`.
|
Associated.irreducible
theorem Associated.irreducible :
∀ {α : Type u_1} [inst : Monoid α] {p q : α}, Associated p q → Irreducible p → Irreducible q
This theorem states that for any type `α` which has a `Monoid` structure, if two elements `p` and `q` of this structure are associated (meaning there exists a unit `u` such that `p` multiplied by `u` equals `q`), then if `p` is irreducible, `q` must be irreducible as well. In mathematical terms, irreducibility is preserved under association in a monoid.
More concisely: If `α` is a type with a `Monoid` structure and `p` and `q` are associates in `α` with a common unit `u`, then `p` irreducible implies `q` is irreducible.
|
associated_eq_eq
theorem associated_eq_eq : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Unique αˣ], Associated = Eq
The theorem `associated_eq_eq` states that for any type `α` that forms a `Monoid`, and has a property that it is `Unique` (meaning there's exactly one unit element), the relation `Associated` is equivalent to the equality relation. In other words, two elements of the `Monoid` are `Associated` if and only if they are equal. This is because in such a `Monoid`, the only unit is the multiplicative identity, so an element can only be `Associated` (multiplied by a unit to get another) with itself.
More concisely: In a Monoid with a unique unit, the relation of being Associated coincides with equality.
|
Prime.not_unit
theorem Prime.not_unit : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : α}, Prime p → ¬IsUnit p
This theorem states that for any commutative monoid with zero, an element `p` being prime implies that `p` is not a unit. In other words, any prime element in a commutative monoid with zero does not have a two-sided inverse, or equivalently, cannot be written as the product of a unit and some other element.
More concisely: In a commutative monoid with zero, a prime element has no multiplicative inverse.
|
Associates.dvd_eq_le
theorem Associates.dvd_eq_le : ∀ {α : Type u_1} [inst : CommMonoid α], (fun x x_1 => x ∣ x_1) = fun x x_1 => x ≤ x_1
This theorem states that for any type `α` that is a commutative monoid, the "divides" relation (`x` divides `x_1`) is equivalent to the "less than or equal to" relation (`x` is less than or equal to `x_1`). In other words, for any two elements in a commutative monoid, saying that one element divides the other is the same as saying that the one element is less than or equal to the other.
More concisely: In a commutative monoid, the relation `x` divides `x_1` is equivalent to `x` being less than or equal to `x_1`.
|
Associates.dvd_of_mk_le_mk
theorem Associates.dvd_of_mk_le_mk :
∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, Associates.mk a ≤ Associates.mk b → a ∣ b
The theorem `Associates.dvd_of_mk_le_mk` states that for any commutative monoid `α`, given any two elements `a` and `b` of `α`, if the canonical quotient map from `a` into the `Associates` of `α` is less than or equal to the canonical quotient map from `b` into the `Associates` of `α`, then `a` divides `b`. In other words, for any two elements of a commutative monoid, if their associated elements in the quotient group are in a certain order, then the original elements have a divisibility relationship.
More concisely: If `α` is a commutative monoid and the canonical quotient of `a` in the `Associates` of `α` is less than or equal to the canonical quotient of `b` in the `Associates` of `α`, then `a` divides `b` in `α`.
|
Associates.dvdNotUnit_iff_lt
theorem Associates.dvdNotUnit_iff_lt :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a b : Associates α}, DvdNotUnit a b ↔ a < b
The theorem `Associates.dvdNotUnit_iff_lt` states that for any type `α` that has a `CancelCommMonoidWithZero` structure, given any two elements `a` and `b` from the set of associates of `α`, `a` divides `b` strictly if and only if `a` is less than `b`.
In other words, in the context of the associated elements of a cancel commutative monoid with zero, an element `a` strictly dividing another element `b` is equivalent to `a` being less than `b`. Here, an element `a` strictly divides `b` (denoted as `DvdNotUnit a b`) if `a` is not zero and there exists an element `x` such that `x` is not a unit and `b = a * x`.
More concisely: For any cancel commutative monoid with zero `α`, elements `a` and `b` being associates of `α` satisfy `a < b` if and only if `a` strictly divides `b` (i.e., `a ≠ 0` and `b = a * x` for some non-unit `x`).
|
of_irreducible_mul
theorem of_irreducible_mul : ∀ {α : Type u_5} [inst : Monoid α] {x y : α}, Irreducible (x * y) → IsUnit x ∨ IsUnit y
This theorem states that for any type `α` where a monoid structure is defined, if the product of two elements 'x' and 'y' of `α` is irreducible (i.e., in the monoid, it cannot be factored into two non-unit elements), then either 'x' or 'y' must be a unit. A unit is an element that has a two-sided inverse in the monoid.
More concisely: In a monoid, if the product of two irreducible elements is irreducible, then one of them is a unit.
|
Associates.mk_eq_mk_iff_associated
theorem Associates.mk_eq_mk_iff_associated :
∀ {α : Type u_1} [inst : Monoid α] {a b : α}, Associates.mk a = Associates.mk b ↔ Associated a b
This theorem states that for any type `α` that forms a `Monoid`, two elements `a` and `b` of `α` have the same `Associates` via the `Associates.mk` function if and only if `a` and `b` are `Associated`. In mathematical terms, `a` and `b` are `Associated` if there exists a unit `u` such that `a` multiplied by `u` equals `b`.
More concisely: For any monoid type `α` and elements `a` and `b` of `α`, `a` and `b` have the same associates if and only if they are associated through a unit.
|
Associated.trans
theorem Associated.trans :
∀ {α : Type u_1} [inst : Monoid α] {x y z : α}, Associated x y → Associated y z → Associated x z
The theorem `Associated.trans` states that for any type `α` that is a `Monoid`, the `Associated` relation is transitive. In other words, if `x` and `y` are associated elements in the monoid, and `y` and `z` are also associated, then `x` and `z` are associated. Here, two elements are associated if one is the product of the other and a unit of the monoid.
More concisely: For any monoid `α`, if `x` is associated with `y` and `y` is associated with `z`, then `x` is associated with `z`.
|
eq_of_prime_pow_eq
theorem eq_of_prime_pow_eq :
∀ {R : Type u_5} [inst : CancelCommMonoidWithZero R] [inst_1 : Unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ},
Prime p₁ → Prime p₂ → 0 < k₁ → p₁ ^ k₁ = p₂ ^ k₂ → p₁ = p₂
The theorem `eq_of_prime_pow_eq` states that, for any type `R` that forms a cancel commutative monoid with 0 and possesses a unique unit, given two elements `p₁` and `p₂` from `R` and two non-zero natural numbers `k₁` and `k₂`. If `p₁` and `p₂` are both prime elements in the sense that they are non-zero, not a unit, and for any two elements `a` and `b` from `R`, if the prime element divides the product of `a` and `b`, then it divides either `a` or `b`, and the `k₁`-th power of `p₁` equals the `k₂`-th power of `p₂`, then `p₁` must equal `p₂`.
More concisely: If two non-unit, prime elements `p₁` and `p₂` in a cancel commutative monoid `R` with 0 and a unique unit, satisfied `p₁^k₁ = p₂^k₂` for some non-zero natural numbers `k₁` and `k₂`, then `p₁` equals `p₂`.
|
Associates.mk_ne_zero
theorem Associates.mk_ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] {a : α}, Associates.mk a ≠ 0 ↔ a ≠ 0 := by
sorry
This theorem states that for any type `α` that is a monoid with zero, a term `a` of type `α` is mapped to a non-zero element in the `Associates` of `α` if and only if `a` is not zero. In other words, the function `Associates.mk` preserves the non-zero property when mapping from a monoid to its associates.
More concisely: For any monoid with zero `α` and non-zero element `a` of type `α`, `a` is mapped to a non-zero associate by `Associates.mk`.
|
Associated.dvd
theorem Associated.dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, Associated a b → a ∣ b
This theorem states that, for any type `α` that is a Monoid, if two elements `a` and `b` of `α` are associated (i.e., `a` can be expressed as `b` multiplied by a unit on the right), then `a` divides `b`. In math notation, this would be "if a and b are associated (there exists a unit u such that a * u = b), then a divides b".
More concisely: If `α` is a monoid and there exists a unit `u` such that `a = b * u`, then `a` divides `b`.
|
Associated.prime_iff
theorem Associated.prime_iff :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p q : α}, Associated p q → (Prime p ↔ Prime q)
The theorem `Associated.prime_iff` states that for any type `α` that is a commutative monoid with zero, and any two elements `p` and `q` of `α`, if `p` and `q` are associated (meaning one can be obtained by multiplying the other by a unit), then `p` is a prime element if and only if `q` is a prime element. A prime element in this context is an element that is not zero, not a unit, and if it divides the product of two other elements, then it must divide at least one of them.
More concisely: If `p` and `q` are associated elements in a commutative monoid with zero, then `p` is prime if and only if `q` is prime.
|
irreducible_iff
theorem irreducible_iff :
∀ {α : Type u_1} [inst : Monoid α] {p : α},
Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b
The theorem `irreducible_iff` states that for any type `α` that is a `Monoid`, an element `p` of `α` is irreducible if and only if it is not a unit and for any two elements `a` and `b` of `α`, if `p` is equal to the product of `a` and `b`, then either `a` or `b` is a unit. Here, a unit in a monoid is an element that has a two-sided inverse.
More concisely: An element `p` of a monoid `α` is irreducible if and only if it is not a unit and there does not exist non-unit elements `a` and `b` in `α` such that `p = a * b`.
|
not_irreducible_zero
theorem not_irreducible_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α], ¬Irreducible 0
This theorem states that zero is not irreducible for any type `α` provided that `α` is a monoid with zero. In mathematical terms, an element in a monoid is called irreducible if it is non-zero and cannot be expressed as a product of two non-unit elements. Thus, according to this theorem, zero does not meet these criteria and is therefore not considered irreducible in the context of a monoid with zero.
More concisely: In a monoid with zero, zero is not an irreducible element.
|
Irreducible.isUnit_or_isUnit
theorem Irreducible.isUnit_or_isUnit :
∀ {α : Type u_1} [inst : Monoid α] {p : α}, Irreducible p → ∀ {a b : α}, p = a * b → IsUnit a ∨ IsUnit b
This theorem states that for any type `α` that has a `Monoid` structure, given an element `p` of `α` that is irreducible, if `p` can be expressed as the product of two elements `a` and `b` of `α`, then either `a` or `b` is a unit. In terms of group theory, a unit is an element which has a two-sided inverse. In other words, if an irreducible element can be factored, then one of the factors must have an inverse, which in the context of multiplication, means that one of them is a unit.
More concisely: For any irreducible element `p` of a `Monoid` type `α`, if `p` can be written as the product of elements `a` and `b` in `α`, then exactly one of `a` or `b` is a unit.
|
Irreducible.dvd_symm
theorem Irreducible.dvd_symm :
∀ {α : Type u_1} [inst : Monoid α] {p q : α}, Irreducible p → Irreducible q → p ∣ q → q ∣ p
This theorem states that for any type `α` that is a monoid, if `p` and `q` are elements of `α` that are irreducible, then if `p` divides `q`, it must also be the case that `q` divides `p`. Here, "divides" means that there is some element in the monoid such that multiplying that element by `p` gives `q`, and similarly for `q` divides `p`. An irreducible element is one that cannot be expressed as the product of two non-unit elements.
More concisely: In a monoid, if two irreducible elements `p` and `q` satisfy `p` divides `q`, then `q` also divides `p`.
|
Prime.ne_zero
theorem Prime.ne_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : α}, Prime p → p ≠ 0
The theorem `Prime.ne_zero` states that for any type `α` that has a `CommMonoidWithZero` structure, a prime element `p` of type `α` is not equal to zero. In other words, if `p` is a prime element in a commutative monoid with zero, then `p` cannot be zero.
More concisely: In a commutative monoid with zero, a prime element is distinct from zero.
|
associated_zero_iff_eq_zero
theorem associated_zero_iff_eq_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), Associated a 0 ↔ a = 0 := by
sorry
The theorem `associated_zero_iff_eq_zero` states that for any type `α` that has the structure of a `MonoidWithZero`, an element `a` of type `α` is "associated" with zero if and only if `a` is zero itself. In the context of monoids, two elements are typically "associated" if one can be obtained from the other by multiplication with a unit. However, in a `MonoidWithZero`, the only way for an element to be associated with zero is if the element is zero itself, since multiplying any non-zero element by a unit cannot yield zero.
More concisely: In a MonoidWithZero type, an element is associated with zero if and only if it is equal to zero.
|
Mathlib.Algebra.Associated._auxLemma.19
theorem Mathlib.Algebra.Associated._auxLemma.19 :
∀ {α : Type u_1} [inst : Monoid α] {a b u : α}, IsUnit u → (a * u ∣ b) = (a ∣ b)
The theorem `Mathlib.Algebra.Associated._auxLemma.19` asserts that for any type `α` that has a Monoid structure, and any property `p` defined on the `Associates` of `α`, stating that this property holds for all elements in the `Associates` of `α` is equivalent to stating that the property holds for all elements in `α` after they are mapped into the `Associates` of `α` by the canonical quotient map `Associates.mk`. In other words, a property is true for all associates if and only if it is true for all original elements before being transformed by `Associates.mk`.
More concisely: For any monoid `α` and property `p` on its associates, `p` holds for all associates if and only if it holds for all elements of `α` after being quotiented by the associates relation.
|
Associated.prime
theorem Associated.prime :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p q : α}, Associated p q → Prime p → Prime q
This theorem states that for any commutative monoid with zero, if two elements 'p' and 'q' are associated and 'p' is a prime element, then 'q' is also a prime element. Here, an element is said to be prime if it is non-zero, is not a unit, and if it divides a product of two elements, it must divide at least one of them. Two elements are associated if one can be obtained by multiplying the other by a unit element.
More concisely: If two commutative monoid elements 'p' and 'q' are associated and 'p' is prime, then 'q' is also prime.
|
associated_one_iff_isUnit
theorem associated_one_iff_isUnit : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, Associated a 1 ↔ IsUnit a
This theorem states that for any type `α` that forms a `Monoid`, an element `a` of `α` is associated with 1 if and only if `a` is a unit. In mathematical terms, in the context of a given monoid, an element `a` is associated with the identity element (denoted by 1 here) if there exists a unit such that `a` multiplied by this unit equals to the identity. This is equivalent to saying that `a` is a unit itself, meaning there exists some unit such that when this unit is dereferenced, it equals to `a`.
More concisely: In a monoid, an element is associated with the identity if and only if it is a unit.
|
irreducible_mul_isUnit
theorem irreducible_mul_isUnit :
∀ {α : Type u_1} [inst : Monoid α] {a b : α}, IsUnit a → (Irreducible (b * a) ↔ Irreducible b)
The theorem `irreducible_mul_isUnit` states that for any type `α` that is a monoid (denoted as `Monoid α`), and for any two elements `a` and `b` of this monoid (denoted as `a, b : α`), if `a` is a unit in this monoid (which means `a` has a two-sided inverse, denoted as `IsUnit a`), then `b * a` is irreducible if and only if `b` is irreducible. In mathematical terms, an element `b` in a monoid is called irreducible if and only if it cannot be expressed as a product of two non-unit elements.
More concisely: For any monoid `α` and elements `a` and `b` in `α` with `IsUnit a`, `b` is irreducible if and only if `b * a` is irreducible.
|
Irreducible.associated_of_dvd
theorem Irreducible.associated_of_dvd :
∀ {α : Type u_1} [inst : Monoid α] {p q : α}, Irreducible p → Irreducible q → p ∣ q → Associated p q
This theorem states that for any type `α` that forms a `Monoid`, given two elements `p` and `q` of this type, if both `p` and `q` are irreducible and `p` divides `q`, then `p` and `q` are associated. In terms of number theory, two elements are associated if they differ by a multiplication of a unit, which in the case of integers, means they are multiples of each other. Thus, the theorem is asserting that in a monoid, two irreducible elements that divide each other must be associates.
More concisely: In a monoid, if two irreducible elements are divisors of each other, then they are associates.
|
irreducible_iff_prime
theorem irreducible_iff_prime :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : DecompositionMonoid α] {a : α},
Irreducible a ↔ Prime a
The theorem `irreducible_iff_prime` states that for any type `α` that is a cancellative commutative monoid with zero and also a decomposition monoid, an element `a` of `α` is irreducible if and only if it is prime.
In mathematical terms, this means that in this specific algebraic structure (a cancellative commutative monoid with zero that has a decomposition monoid structure), an element is irreducible (cannot be factored into two non-unit elements) if and only if it is prime (it is not zero, it is not a unit, and whenever it divides a product, it divides at least one of the factors).
More concisely: In a cancellative commutative monoid with zero and decomposition monoid structure, an element is irreducible if and only if it is prime.
|
Irreducible.prime
theorem Irreducible.prime :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecompositionMonoid α] {a : α}, Irreducible a → Prime a
This theorem states that for any type `α` that is a Commutative Monoid with Zero and can be decomposed (i.e., it has the properties of a `DecompositionMonoid`), any irreducible element `a` of type `α` is also a prime element. In mathematical terms, for a commutative monoid with zero and decomposition property, if an element is irreducible, then it's also prime. An irreducible element `a` is one that can't be expressed as a product of two non-unit elements, while a prime element `p` is a non-zero, non-unit element that satisfies the property that if `p` divides the product of `a` and `b`, then `p` must divide `a` or `b`.
More concisely: In a commutative monoid with zero and decomposition property, every irreducible element is prime.
|
Associates.mk_le_mk_iff_dvd_iff
theorem Associates.mk_le_mk_iff_dvd_iff :
∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, Associates.mk a ≤ Associates.mk b ↔ a ∣ b
The theorem `Associates.mk_le_mk_iff_dvd_iff` states that for any type `α` which is a commutative monoid, and for any two elements `a` and `b` of type `α`, the statement that the associate of `a` is less than or equal to the associate of `b` is equivalent to the statement that `a` divides `b`. In other words, it provides a connection between the ordering in the associates of a commutative monoid and the divisibility relation in the original monoid.
More concisely: For any commutative monoid type `α`, the relation `a ∘ x = b ∘ y` implies `a = y * x ⊢ b = x * z → a | b` (associate of `a` is less than or equal to associate of `b` if and only if `a` divides `b`).
|
Associates.irreducible_mk
theorem Associates.irreducible_mk :
∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a : α}, Irreducible (Associates.mk a) ↔ Irreducible a
The theorem `Associates.irreducible_mk` states that for all types `α` that are equipped with a `CommMonoidWithZero` structure, a given element `a` of type `α` is irreducible in the associated monoid if and only if `a` itself is irreducible in the original monoid `α`. In simple terms, it's stating that the irreducibility of an element doesn't change when we move from the original monoid to its associated monoid.
More concisely: For any type `α` with a `CommMonoidWithZero` structure, an element `a` is irreducible in the associated monoid if and only if it is irreducible in the original monoid `α`.
|
Associated.refl
theorem Associated.refl : ∀ {α : Type u_1} [inst : Monoid α] (x : α), Associated x x
This theorem states that for any given type `α` that forms a Monoid (a set equipped with an associative binary operation and an identity element), any element `x` of this type is associated with itself. In other words, there exists a unit such that when it is multiplied by `x` on the right, the result is `x` itself. This is a reflection property of the `Associated` relation in a Monoid.
More concisely: For any monoid `α` and its element `x`, there exists an identity element `e` such that `x * e = x`.
|
Associated.mul_right
theorem Associated.mul_right :
∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, Associated a b → ∀ (c : α), Associated (a * c) (b * c)
The theorem `Associated.mul_right` states that for all types `α` in a commutative monoid, if two elements `a` and `b` are associated, then for any other element `c` in the same monoid, the product of `a` and `c`, and the product of `b` and `c` are also associated. "Associated" here means that one element can be obtained by multiplying the other by a unit on the right.
More concisely: If `a` and `b` are associated elements in a commutative monoid `α`, then for all `c` in `α`, the products `a * c` and `b * c` are also associated.
|
Irreducible.ne_zero
theorem Irreducible.ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] {p : α}, Irreducible p → p ≠ 0
This theorem states that for any type `α` (with the condition that `α` is a monoid with zero), an element `p` of type `α` that is irreducible cannot be equal to zero. In mathematical terms, if `p` is an irreducible element of a monoid with zero, then `p` must be a non-zero element.
More concisely: If `α` is a monoid with zero, then any irreducible element `p` in `α` is non-zero.
|
Associates.one_le
theorem Associates.one_le : ∀ {α : Type u_1} [inst : CommMonoid α] {a : Associates α}, 1 ≤ a
The theorem `Associates.one_le` states that, for any commutative monoid `α` and any element `a` of the set of associates of `α`, the monoid unit (1) is less than or equal to `a`. In other words, for any `a` in the quotient of a commutative monoid by the associated relation (two elements `x` and `y` are associated if there is a unit `u` such that `x * u = y`), `1` is not greater than `a`.
More concisely: For any commutative monoid and any element in its associated equivalence class, the monoid unit is less than or equal to that element.
|