lcm_same
theorem lcm_same :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α),
lcm a a = normalize a
The theorem `lcm_same` states that for any type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, and for any element `a` of type `α`, the least common multiple (LCM) of `a` and `a` is equal to the normalized value of `a`. In other words, when the two inputs to the LCM function are the same, the output is simply the input multiplied by the norm unit of the input.
More concisely: For any cancel commutative monoid with zero and normalized GCD monoid type `α`, the LCM of an element `a` equals the normalized value of `a`. That is, LCM(a, a) = norm a.
|
dvd_gcd_iff
theorem dvd_gcd_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b c : α),
a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c
This theorem, `dvd_gcd_iff`, states that for any type `α` that is a cancelable commutative monoid with zero and has a Greatest Common Divisor (GCD) structure, a given element `a` of `α` divides the GCD of two other elements `b` and `c` if and only if `a` divides both `b` and `c`. In mathematical terms, $a | gcd(b, c)$ if and only if $a | b$ and $a | c$.
More concisely: For any cancelable commutative monoid with zero and a GCD structure, an element divides the GCD of two other elements if and only if it divides both elements.
|
normalize_one
theorem normalize_one :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α], normalize 1 = 1
The theorem `normalize_one` states that for any type `α` that has a `CancelCommMonoidWithZero` and a `NormalizationMonoid` structure, the `normalize` function applied to the multiplicative identity `1` yields `1`. In other words, normalizing `1` does not change its value in any such algebraic structure.
More concisely: For any type `α` equipped with both a `CancelCommMonoidWithZero` and a `NormalizationMonoid` structure, the normalization of the multiplicative identity `1` is equal to `1`.
|
NormalizedGCDMonoid.normalize_lcm
theorem NormalizedGCDMonoid.normalize_lcm :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : NormalizedGCDMonoid α] (a b : α),
normalize (lcm a b) = lcm a b
This theorem states that for any given type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, and for any two elements `a` and `b` of this type, the least common multiple (LCM) of `a` and `b` is invariant under normalization. In other words, normalizing the least common multiple (LCM) of `a` and `b` results in the LCM of `a` and `b` itself.
More concisely: For any cancel commutative monoid with zero and a normalized GCD monoid `α`, the normalization of the least common multiple of two elements `a` and `b` is equal to the least common multiple of `a` and `b` itself.
|
gcd_zero_left
theorem gcd_zero_left :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α),
gcd 0 a = normalize a
The theorem `gcd_zero_left` states that for any type `α` that has an instance of the `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` structures, for any element `a` of type `α`, the greatest common divisor (gcd) of 0 and `a` is equal to the normalized form of `a`. In other words, in the context of a cancel commutative monoid with zero and normalized GCD monoid structure, the gcd of zero and any element is just the normalized version of the element itself.
More concisely: In a cancel commutative monoid with zero and normalized GCD monoid structures, the greatest common divisor of 0 and any element is equal to the normalized form of that element.
|
GCDMonoid.lcm_zero_right
theorem GCDMonoid.lcm_zero_right :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] (a : α), lcm a 0 = 0
This theorem states that zero is right-absorbing with respect to the least common multiple (LCM) operation in a GCDMonoid. Specifically, for any type `α` that has both a CancelCommMonoidWithZero and a GCDMonoid structure, and for any element `a` of that type, the least common multiple of `a` and `0` is `0`. Essentially, when you take the least common multiple of any number and zero, you always get zero.
More concisely: In a GCDMonoid with CancelCommMonoidWithZero structure, the least common multiple of any element and zero is zero.
|
associated_normalize
theorem associated_normalize :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
Associated x (normalize x)
The theorem `associated_normalize` states that for any type `α` that forms a `CancelCommMonoidWithZero` and a `NormalizationMonoid`, every element `x` of type `α` is `Associated` with its normalized form. In other words, `x` and `normalize x` are `Associated` for any `x` in such a type `α`. Here, two elements are said to be `Associated` if one can be obtained by multiplying the other with a unit from the right. The normalization process is achieved by multiplying an element with the `normUnit` of the `NormalizationMonoid`.
More concisely: For any type `α` that is a `CancelCommMonoidWithZero` and has a `NormalizationMonoid`, every element `x` in `α` is associated to its normalized form `normalize x`.
|
gcd_eq_normalize
theorem gcd_eq_normalize :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a b c : α},
gcd a b ∣ c → c ∣ gcd a b → gcd a b = normalize c
The theorem `gcd_eq_normalize` asserts that for any type `α` that forms a cancel commutative monoid with zero and is also a normalized gcd monoid, and for any three elements `a`, `b`, and `c` of `α`, if the greatest common divisor (gcd) of `a` and `b` divides `c` and `c` also divides the gcd of `a` and `b`, then the gcd of `a` and `b` is equal to the normalized value of `c`. Here, the normalization of `c` is achieved by multiplying `c` by the unit-normal of `c`, which essentially "chooses" an element from each associate class.
More concisely: If `α` is a cancel commutative monoid with zero and a normalized gcd monoid, then the gcd of `a` and `b` equals the normalized value of `c`, where `c` is the greatest common divisor of `a` and `b` that divides both `a` and `b`.
|
NormalizationMonoid.normUnit_zero
theorem NormalizationMonoid.normUnit_zero :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : NormalizationMonoid α], normUnit 0 = 1
The theorem `NormalizationMonoid.normUnit_zero` states that for any type `α` that is a Cancel Commutative Monoid with zero and also a Normalization Monoid, the function `normUnit` when applied to `0` (the zero element of the monoid), returns `1` (the identity element of the monoid).
More concisely: For any cancel commutative monoid with zero and normalization monoid structure, the normalization of its zero element is the identity element.
|
normalize_dvd_iff
theorem normalize_dvd_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
normalize a ∣ b ↔ a ∣ b
The theorem `normalize_dvd_iff` states that for any type `α` which is a cancel commutative monoid with zero and also a normalization monoid, and for any two elements `a` and `b` of type `α`, `a` divides `b` if and only if the normalized form of `a` divides `b`. Here, "normalizing" an element means multiplying it by the normalized unit of the monoid, which is a process that essentially adjusts its "size" without changing its "shape" or associate class in the monoid.
More concisely: For any cancel commutative monoid with zero and normalization monoid type `α`, `a` divides `b` if and only if the normalized form of `a` divides the normalized form of `b`.
|
GCDMonoid.gcd_dvd_left
theorem GCDMonoid.gcd_dvd_left :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] (a b : α), gcd a b ∣ a
This theorem states that for any type `α` that forms a Cancel Commutative Monoid with zero, and for which a greatest common divisor (GCD) can be defined (i.e., it forms a `GCDMonoid`), the GCD of any two elements `a` and `b` of this type is a divisor of the first element `a`. In mathematical terms, $\text{gcd}(a, b) | a$ for all `a` and `b` in `α`.
More concisely: For any cancellative commutative monoid `α` with zero and defined GCD, the GCD of any two elements `a` and `b` in `α` is a divisor of `a`.
|
Associated.gcd_eq_right
theorem Associated.gcd_eq_right :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {m n : α},
Associated m n → ∀ (k : α), gcd k m = gcd k n
The theorem `Associated.gcd_eq_right` states that for any type `α` that is a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, and for any elements `m` and `n` of `α` such that `m` is associated with `n`, the greatest common divisor (gcd) of `k` and `m` is equal to the gcd of `k` and `n` for any `k` in `α`. In other words, if `m` and `n` are associated in such a monoid, then computing the gcd by pairing either `m` or `n` with a given third element `k` yields the same result.
More concisely: If `α` is a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid` where `m` and `n` are associated elements, then `gcd m k = gcd n k`.
|
normalize_lcm
theorem normalize_lcm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
normalize (lcm a b) = lcm a b
The theorem `normalize_lcm` states that for any type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, and for any elements `a` and `b` of `α`, the normalized least common multiple (LCM) of `a` and `b` is equal to the LCM of `a` and `b`. In other words, the operation of normalizing the LCM doesn't change its value in a normalized GCD monoid.
More concisely: In a cancel commutative monoid with zero and a normalized GCD monoid, the normalized LCM of two elements is equal to the unnormalized LCM.
|
GCDMonoid.gcd_dvd_right
theorem GCDMonoid.gcd_dvd_right :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] (a b : α), gcd a b ∣ b
This theorem states that for any type `α` that is a commutative monoid with zero and has a greatest common divisor (GCD) function, the GCD of any two elements `a` and `b` of this type is a divisor of `b`. In mathematical terms, if `gcd(a, b)` is the greatest common divisor of `a` and `b`, then `b` is a multiple of `gcd(a, b)`.
More concisely: If `α` is a commutative monoid with zero and has a GCD function, then for all `a, b ∈ α`, `gcd(a, b)` is a divisor of `b`.
|
NormalizedGCDMonoid.normalize_gcd
theorem NormalizedGCDMonoid.normalize_gcd :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : NormalizedGCDMonoid α] (a b : α),
normalize (gcd a b) = gcd a b
The theorem `NormalizedGCDMonoid.normalize_gcd` states that for any type `α` which has a structure of a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, and for any two elements `a` and `b` of that type, the greatest common divisor (gcd) of `a` and `b` when normalized - i.e., multiplied by the multiplicative inverse of its associated unit - is equal to the gcd of `a` and `b` itself. In other words, the gcd of any two elements in a `NormalizedGCDMonoid` is already in its normalized form.
More concisely: In a `NormalizedGCDMonoid`, the normalized greatest common divisor of two elements equals their standard greatest common divisor.
|
normalize_eq
theorem normalize_eq :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Unique αˣ] (x : α), normalize x = x
The theorem `normalize_eq` states that for any given type `α` that is equipped with a cancel-commutative monoid with a zero element, and a unique invertible element (units), the normalization of any element `x` of type `α` is equal to `x` itself. In other words, for such types `α`, the process of normalization does not change the value of the elements.
More concisely: For types `α` equipped with a cancel-commutative monoid and units, the normalization of any element `x` is equal to `x`.
|
gcd_one_right
theorem gcd_one_right :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd a 1 = 1 := by
sorry
This theorem states that for any type 'α' that is a CancelCommMonoidWithZero and a NormalizedGCDMonoid, the greatest common divisor (gcd) of any element 'a' of type 'α' and 1 is always 1. The CancelCommMonoidWithZero and NormalizedGCDMonoid are algebraic structures with specific properties, and the theorem essentially says that 1 is the gcd for any number and 1 in these structures.
More concisely: For any type 'α' that is both a CancelCommMonoidWithZero and a NormalizedGCDMonoid, the greatest common divisor of any element 'a' of type 'α' and 1 is equal to 1.
|
gcd_dvd_gcd
theorem gcd_dvd_gcd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d : α},
a ∣ b → c ∣ d → gcd a c ∣ gcd b d
This theorem states that for any type `α` that is a cancel commutative monoid with zero and also a Greatest Common Divisor (gcd) monoid, and for any elements `a`, `b`, `c`, and `d` of `α`, if `a` divides `b` and `c` divides `d`, then the gcd of `a` and `c` divides the gcd of `b` and `d`. Here, "divides" means that there exists another element of `α` such that multiplying that element by the divisor yields the dividend.
More concisely: If `α` is a cancel commutative monoid with zero and has the gcd operation, then the gcd of `a` and `c` divides the gcd of `b` and `d` whenever `a` divides `b` and `c` divides `d`.
|
gcd_zero_right
theorem gcd_zero_right :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α),
gcd a 0 = normalize a
The theorem `gcd_zero_right` states that for any type `α` equipped with a structure of a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, for any element `a` of type `α`, the greatest common divisor of `a` and `0` equals to the normalized version of `a`. In other words, it says that in this mathematical structure, the gcd of any element and zero is just that element, but normalized (multiplied by the associated unit normal for that element). This is a generalization of the concept that the gcd of any number and zero is the absolute value of that number.
More concisely: For any type `α` with `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` structures, the normalized version of an element `a` is the greatest common divisor of `a` and `0`.
|
normalize_associated
theorem normalize_associated :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
Associated (normalize x) x
The theorem `normalize_associated` states that for any type `α` that has both a `CancelCommMonoidWithZero` and a `NormalizationMonoid` structure, and for any element `x` of type `α`, the `normalize` of `x` is associated with `x`. In the context of monoids, two elements are associated if one can be obtained by multiplying the other by a unit on the right. Here, 'normalize' chooses an element of each associate class by multiplying by `normUnit`. Therefore, this theorem is saying that the normalization of an element is in the same associate class as the original element.
More concisely: For any type `α` with both a `CancelCommMonoidWithZero` and a `NormalizationMonoid` structure, the normalization of an element `x` is in the same associate class.
|
gcdMonoidOfLCM.proof_1
theorem gcdMonoidOfLCM.proof_1 :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] (lcm : α → α → α),
(∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a) → ∀ (a b : α), lcm a b ∣ a * b
This theorem states that for any type `α` that forms a cancel commutative monoid with zero and for any `lcm` function (least common multiple), if for all `a`, `b`, and `c` of type `α`, `c` divides `a` and `b` divides `a` implies that the `lcm` of `c` and `b` divides `a`, then for any `a` and `b` of type `α`, the `lcm` of `a` and `b` divides the product of `a` and `b`. In more mathematical terms, it states that if for all `c`, `b`, `a` in `α`, `c | a` and `b | a` implies `lcm(c,b) | a`, then for any `a`, `b` in `α`, `lcm(a,b) | a*b`.
More concisely: If `α` is a cancel commutative monoid with zero and for all `a`, `b`, `c` in `α`, `c` divides `a` and `b` divides `a` implies that the least common multiple of `c` and `b` divides the product of `a` and `b`, then for all `a`, `b` in `α`, the least common multiple of `a` and `b` divides the product `a * b`.
|
Associates.out_dvd_iff
theorem Associates.out_dvd_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α) (b : Associates α),
b.out ∣ a ↔ b ≤ Associates.mk a
The theorem `Associates.out_dvd_iff` states a property relating the division operation in a `CancelCommMonoidWithZero` and the order operation in the `Associates` of the monoid. For any `CancelCommMonoidWithZero` α and `NormalizationMonoid` α, and any element `a` of α and `b` of `Associates` α, the normalized element of `b`'s associate class divides `a` if and only if `b` is less than or equal to the quotient map of `a` into `Associates` α. In other words, there is a correspondence between the divisibility in the monoid and the order in the quotient by the `Associated` relation.
More concisely: For any `CancelCommMonoidWithZero` α and `NormalizationMonoid` α, the normalized associate of `b` divides `a` in α if and only if `b` is less than or equal to the quotient of `a` modulo the `Associates` relation in α.
|
normalize_gcd
theorem normalize_gcd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
normalize (gcd a b) = gcd a b
The theorem `normalize_gcd` states that for any type `α` that is a Cancel Commutative Monoid with Zero and a Normalized GCD Monoid, and for any two elements `a` and `b` of `α`, the normalized value of the greatest common divisor (gcd) of `a` and `b` is equal to the gcd of `a` and `b` itself. Here, normalization is achieved by multiplying an element by the unit associated with its norm. This shows an important property of the gcd in such a monoid, namely that it is invariant under normalization.
More concisely: For any Cancel Commutative Monoid with Zero and a Normalized GCD Monoid `α`, the normalized gcd of `a` and `b` equals their standard gcd.
|
normalize_eq_one
theorem normalize_eq_one :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] {x : α},
normalize x = 1 ↔ IsUnit x
This theorem, `normalize_eq_one`, states that for any type `α` that is a cancel commutative monoid with zero and a normalization monoid, a given element `x` of type `α` satisfies the property that its normalization equals `1` if and only if `x` is a unit in the monoid. In other words, an element of the monoid is a unit if it has a two-sided inverse and its normalization (which is achieved by multiplying it with the norm unit of `x`) is equal to `1`.
More concisely: For any cancel commutative monoid with zero and a normalization monoid, an element is a unit if and only if its normalization equals the monoid's identity element.
|
Associates.out_mk
theorem Associates.out_mk :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α),
(Associates.mk a).out = normalize a
The theorem `Associates.out_mk` states that for any type `α` that has the structure of a cancel commutative monoid with zero and a normalization monoid, and for every element `a` of `α`, if we first create an associate of `a` using the `Associates.mk` function and then map it back to `α` using the `Associates.out` function, we end up with the normalized form of `a`. In other words, mapping an element to its associate and back again is equivalent to normalizing the element.
More concisely: For any cancel commutative monoid with zero and normalization monoid in type `α`, the normalization of an element `a` is equal to `Associates.out (Associates.mk a)`.
|
normUnit_one
theorem normUnit_one :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α], normUnit 1 = 1
This theorem states that for any type `α` that is a `CancelCommMonoidWithZero` and a `NormalizationMonoid`, the normalization of the unit `1` is `1`. In mathematical terms, if we have a cancellative commutative monoid with zero and a normalization monoid, the norm of the multiplicative identity (which is `1`) always equals `1`.
More concisely: For any cancellative commutative monoid with zero and normalization monoid, the normalization of the multiplicative identity equals 1.
|
normalize_idem
theorem normalize_idem :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
normalize (normalize x) = normalize x
The theorem `normalize_idem` states that for any type `α` that forms a Cancel Commutative Monoid with zero and has a Normalization Monoid structure, the operation `normalize` is idempotent on any element `x` of `α`. That is, applying the `normalize` operation twice on `x` is the same as applying it once. This means the `normalize` operation doesn't change the value of `x` after its first application, irrespective of how many more times it's applied afterwards.
More concisely: For any cancel commutative monoid `α` with zero and a normalization monoid structure, the normalization operation is idempotent.
|
gcd_mul_lcm
theorem gcd_mul_lcm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α),
Associated (gcd a b * lcm a b) (a * b)
This theorem states that for any type `α` that is a `CancelCommMonoidWithZero` and a `GCDMonoid`, and for any two elements `a` and `b` of type `α`, the Greatest Common Divisor (gcd) of `a` and `b` multiplied by the Least Common Multiple (lcm) of `a` and `b` is associated with the product of `a` and `b`. In other words, there exists a unit `u` such that `(gcd a b * lcm a b) * u = a * b`. Here, `Associated` is defined as a relationship where two elements of the type `α` are associated if one is the product of the other and a unit from the Monoid.
More concisely: For any `CancelCommMonoidWithZero` and `GCDMonoid` type `α` and elements `a, b ∈ α`, there exists a unit `u` such that `gcd a b * lcm a b * u = a * b`.
|
gcd_eq_zero_iff
theorem gcd_eq_zero_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α),
gcd a b = 0 ↔ a = 0 ∧ b = 0
This theorem states that for any type `α` that is a cancel commutative monoid with zero and a GCD monoid, the greatest common divisor (gcd) of two values `a` and `b` of this type equals zero if and only if both `a` and `b` are zero. In mathematical terms, for all `a` and `b` in `α`, gcd(`a`, `b`) = 0 is equivalent to `a` = 0 and `b` = 0.
More concisely: For any cancel commutative monoid with zero and a GCD operation, the greatest common divisor of two elements is equal to zero if and only if both elements are zero.
|
normalize_zero
theorem normalize_zero :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α], normalize 0 = 0
This theorem states that for any type `α` that is a member of the classes `CancelCommMonoidWithZero` and `NormalizationMonoid`, the normalization of zero is zero. In more mathematical terms, if we have a cancel commutative monoid with zero (a structure with zero where multiplication is commutative and cancellative) and a normalization monoid (a structure with a function that returns 'normalized' elements) then the normalization operation applied to zero will always return zero.
More concisely: For any type `α` that is a cancel commutative monoid with zero and a normalization monoid, the normalization of zero is zero.
|
lcm_eq_normalize
theorem lcm_eq_normalize :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a b c : α},
lcm a b ∣ c → c ∣ lcm a b → lcm a b = normalize c
The theorem `lcm_eq_normalize` states that for any type `α` equipped with a `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` structures, and for any three elements `a`, `b`, and `c` of type `α`, if the least common multiple (lcm) of `a` and `b` divides `c` and `c` divides the lcm of `a` and `b`, then the lcm of `a` and `b` is equal to the normalized form of `c`. The normalization is achieved by multiplying `c` with the inverse of its associated unit.
More concisely: If `a`, `b`, and `c` are elements of a type `α` with `CancelCommMonoidWithZero` and `NormalizedGCDMonoid` structures, and the lcm of `a` and `b` divides both `c` and the normalized form of `c`, then the lcm of `a` and `b` equals the normalized form of `c`.
|
lcm_units_coe_left
theorem lcm_units_coe_left :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (u : αˣ) (a : α),
lcm (↑u) a = normalize a
The theorem `lcm_units_coe_left` states that for any type `α` that is a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, and any unit `u` and element `a` in `α`, the least common multiple of `u` and `a` is equal to the normalization of `a`. In other words, the least common multiple of a unit and any other element in a cancel commutative monoid with zero, which also forms a normalized gcd monoid, is simply the normalized form of the other element.
More concisely: For any unit `u` and element `a` in a cancel commutative monoid with zero and normalized gcd properties, the least common multiple of `u` and `a` equals the normalized form of `a`.
|
lcm_dvd_lcm
theorem lcm_dvd_lcm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d : α},
a ∣ b → c ∣ d → lcm a c ∣ lcm b d
This theorem states that for any type `α` that is a cancellative commutative monoid with zero and a gcd monoid, and for any elements `a`, `b`, `c`, and `d` of that type, if `a` divides `b` and `c` divides `d`, then the least common multiple of `a` and `c` also divides the least common multiple of `b` and `d`.
More concisely: If `α` is a cancellative commutative monoid with zero and a gcd, then for all `a, b, c, d ∈ α`, if `a` divides `b` and `c` divides `d`, then the greatest common divisor of `a` and `c` divides the greatest common divisor of `b` and `d`. (Note: Least common multiples are defined as the reciprocal of greatest common divisors in the context of commutative monoids with zero.)
|
gcd_comm
theorem gcd_comm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
gcd a b = gcd b a
This theorem states that the greatest common divisor (gcd) operation is commutative for any given type `α`, which is a cancel commutative monoid with zero and also a normalized gcd monoid. In other words, for any two elements `a` and `b` of this type, the gcd of `a` and `b` is the same as the gcd of `b` and `a`. This resembles the property in number theory that the order of the two numbers doesn't affect the outcome when computing the gcd.
More concisely: For any type `α` that is a cancel commutative monoid with zero and a normalized gcd monoid, the gcd of `a` and `b` equals the gcd of `b` and `a` for all `a`, `b` in `α`.
|
dvd_antisymm_of_normalize_eq
theorem dvd_antisymm_of_normalize_eq :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
normalize a = a → normalize b = b → a ∣ b → b ∣ a → a = b
This theorem states that for any type `α` that has instances of `CancelCommMonoidWithZero` and `NormalizationMonoid`, and any elements `a` and `b` of that type, if `a` and `b` are normalized (i.e., `normalize a = a` and `normalize b = b`), and `a` divides `b` while `b` divides `a`, then `a` must be equal to `b`. This is essentially an antisymmetry property under division for normalized elements in a normalization monoid with cancellation.
More concisely: If `α` is a type with instances of `CancelCommMonoidWithZero` and `NormalizationMonoid`, and `a` and `b` are normalized elements of `α` such that `a` divides `b` and `b` divides `a`, then `a = b`.
|
normalizedGCDMonoidOfLCM.proof_1
theorem normalizedGCDMonoidOfLCM.proof_1 :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (lcm : α → α → α),
(∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a) → ∀ (a b : α), lcm a b ∣ normalize (a * b)
The theorem `normalizedGCDMonoidOfLCM.proof_1` states that for all types `α` which have a cancel commutative monoid with zero structure and a normalization monoid structure, if you have a function `lcm` (least common multiple), and for all `a`, `b`, and `c` of type `α`, if `c` divides `a` and `b` also divides `a`, then `lcm c b` divides `a`, then for all `a` and `b` of type `α`, the `lcm` of `a` and `b` divides the normalized product of `a` and `b`. Here, normalization is performed by the `normalize` function, which chooses an element from each associate class by multiplying with the norm unit.
More concisely: For all types `α` with a cancel commutative monoid, zero structure, and normalization monoid structure, if `lcm` is a function satisfying the given divisibility condition, then `lcm (normalize a) (normalize b)` divides `normalize (a * b)` for all `a, b` in `α`.
|
lcm_dvd
theorem lcm_dvd :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α},
a ∣ b → c ∣ b → lcm a c ∣ b
This theorem states that for any type `α` that is a cancel commutative monoid with zero and a gcd monoid, and any elements `a`, `b`, `c` of that type, if `a` divides `b` and `c` divides `b`, then the least common multiple (lcm) of `a` and `c` also divides `b`. This theorem essentially captures one of the key properties of the least common multiple in the context of a gcd monoid.
More concisely: If `α` is a cancel commutative monoid with zero and a gcd, then for all `a, b, c` in `α` with `a` dividing `b` and `c` dividing `b`, the least common multiple of `a` and `c` also divides `b`.
|
associatesEquivOfUniqueUnits_apply
theorem associatesEquivOfUniqueUnits_apply :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Unique αˣ] (a : Associates α),
associatesEquivOfUniqueUnits a = a.out
The theorem `associatesEquivOfUniqueUnits_apply` states that for any type `α` that has a cancel-commutative monoid structure with zero and a unique unit (other than one), and for any element `a` of the Associates of `α`, the application of the monoid isomorphism `associatesEquivOfUniqueUnits` on `a` is equivalent to mapping the element `a` back to the normalized element of its associate class using the `Associates.out` function. In other words, the isomorphism `associatesEquivOfUniqueUnits` acts identically to the `Associates.out` function in this context.
More concisely: For any type `α` with a cancel-commutative monoid structure, unique unit, and associates, the monoid isomorphism `associatesEquivOfUniqueUnits` and the function `Associates.out` agree on their application to any associate `a` of the unit.
|
NormalizationMonoid.normUnit_mul
theorem NormalizationMonoid.normUnit_mul :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : NormalizationMonoid α] {a b : α},
a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
This theorem, `NormalizationMonoid.normUnit_mul`, states that for any type `α` that has the structure of a `CancelCommMonoidWithZero` and a `NormalizationMonoid`, and for any two non-zero elements `a` and `b` of this type, the `normUnit` of the product of `a` and `b` is equal to the product of the `normUnit` of `a` and the `normUnit` of `b`. In other words, the `normUnit` function respects the multiplication of non-zero elements in a normalization monoid.
More concisely: For any type endowed with the structures of a CancelCommMonoidWithZero and a NormalizationMonoid, the normUnit of their product equals the product of their respective normUnits, for any non-zero elements.
|
NormalizationMonoid.normUnit_coe_units
theorem NormalizationMonoid.normUnit_coe_units :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : NormalizationMonoid α] (u : αˣ), normUnit ↑u = u⁻¹
This theorem, named `NormalizationMonoid.normUnit_coe_units`, states that for any type `α` that has a `CancelCommMonoidWithZero` and `NormalizationMonoid` structure, the `normUnit` function maps any unit `u` of type `α` to its multiplicative inverse. In other words, for every unit `u` in the normalization monoid `α`, the norm (or absolute value) of `u` is equal to the inverse of `u`. This theorem is part of the `NormalizationMonoid` theory, which deals with the properties of mathematical structures having a normal form or a canonical representation.
More concisely: For any type `α` with `CancelCommMonoidWithZero` and `NormalizationMonoid` structures, the `normUnit` function maps units to their multiplicative inverses.
|
dvd_normalize_iff
theorem dvd_normalize_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
a ∣ normalize b ↔ a ∣ b
The theorem `dvd_normalize_iff` states that for any type `α` that forms a `CancelCommMonoidWithZero` and a `NormalizationMonoid`, and any elements `a` and `b` of this type, `a` divides the normalized form of `b` if and only if `a` divides `b`. Here, "normalizing" an element is achieved by multiplying it with the norm unit of that element, as defined in the `normalize` function.
More concisely: For any type `α` that forms a CancelCommMonoidWithZero and a NormalizationMonoid, `a` divides the normalization of `b` in `α` if and only if `a` divides `b`.
|
gcd_same
theorem gcd_same :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α),
gcd a a = normalize a
The theorem `gcd_same` states that for any type `α` that has the structure of a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, the greatest common divisor (GCD) of any element `a` with itself is equal to the normalized value of `a`. In other words, `gcd(a, a)` equals `normalize(a)`. This is a common property in number theory, and it holds in this general algebraic setting as well.
More concisely: For any type `α` with the structures of a CancelCommMonoidWithZero and a NormalizedGCDMonoid, the normalized value of an element `a` is equal to its greatest common divisor, i.e., `normalize(a) = gcd(a, a)`.
|
dvd_lcm_left
theorem dvd_lcm_left :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), a ∣ lcm a b
This theorem states that for any type `α` which is a cancel commutative monoid with zero and a GCD monoid, and for any elements `a` and `b` of type `α`, `a` divides the least common multiple (LCM) of `a` and `b`. In other words, for all `a` and `b` in the given type, the LCM of `a` and `b` is always a multiple of `a`.
More concisely: For any cancel commutative monoid with zero and a GCD monoid `α`, for all `a, b ∈ α`, `a` divides the least common multiple of `a` and `b`.
|
GCDMonoid.gcd_mul_lcm
theorem GCDMonoid.gcd_mul_lcm :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] (a b : α),
Associated (gcd a b * lcm a b) (a * b)
This theorem states that, in a GCDMonoid, which is a type of special commutative monoid with zero and with the capacity to compute greatest common divisors (GCDs) and least common multiples (LCMs), the product of the GCD and the LCM of any two elements is associated with the product of those two elements. In other words, there exists a unit such that the product of the GCD and the LCM, when multiplied by this unit, equals the product of the two elements. This theorem essentially captures the fundamental relationship between the GCD, the LCM, and the original numbers in the algebraic structure of a GCDMonoid.
More concisely: In a GCDMonoid, the product of the greatest common divisor and least common multiple of any two elements is equal to their product up to a unit.
|
normalize_eq_normalize
theorem normalize_eq_normalize :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
a ∣ b → b ∣ a → normalize a = normalize b
This theorem, `normalize_eq_normalize`, states that for any type `α` that has a `CancelCommMonoidWithZero` and a `NormalizationMonoid` instance, and for any two elements `a` and `b` of this type, if `a` divides `b` and `b` divides `a`, then the normalized form of `a` is equal to the normalized form of `b`.
In mathematical terms, `a` divides `b` and `b` divides `a` means that `a` and `b` are associate elements. The `normalize` function is defining a canonical representative from each associate class, by multiplying each element by the `normUnit` of the element. The theorem is essentially saying that if two elements are associates, they have the same canonical representative.
More concisely: For any type `α` with `CancelCommMonoidWithZero` and `NormalizationMonoid` instances, if `a` and `b` are associates, then their normalized forms are equal.
|
lcm_assoc
theorem lcm_assoc :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (m n k : α),
lcm (lcm m n) k = lcm m (lcm n k)
This theorem states that the least common multiple (LCM) operation is associative for any three elements in a certain type. In other words, for any type `α` that is a `CancelCommMonoidWithZero` and also a `NormalizedGCDMonoid`, and for any three elements `m`, `n`, and `k` of this type, the LCM of the LCM of `m` and `n` with `k` is equal to the LCM of `m` with the LCM of `n` and `k`. This is analogous to the associativity of addition or multiplication in regular arithmetic, where `(a + b) + c = a + (b + c)` or `(a * b) * c = a * (b * c)` respectively.
More concisely: For any type `α` that is both a `CancelCommMonoidWithZero` and a `NormalizedGCDMonoid`, the LCM of `LCM(m, n)` and `k` equals `LCM(m, LCM(n, k))` for all `m, n, k` in `α`.
|
dvd_lcm_right
theorem dvd_lcm_right :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), b ∣ lcm a b
This theorem states that for any type `α` that is a cancel commutative monoid with zero and a GCD monoid, and for any elements `a` and `b` of type `α`, `b` divided by `lcm a b` always holds true. In other words, `b` is always a divisor of the least common multiple of `a` and `b`.
More concisely: For any cancel commutative monoid `α` with zero and a GCD monoid, for all `a, b ∈ α`, `b` divisors `lcm a b`.
|
normalize_apply
theorem normalize_apply :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
normalize x = x * ↑(normUnit x)
This theorem states that for any type 'α' which has the properties of a 'CancelCommMonoidWithZero' and a 'NormalizationMonoid', the operation of 'normalize' applied to an element 'x' of type 'α' is equivalent to multiplying 'x' by the unit norm of 'x'. Here, 'normalize' is a function that chooses an element of each associate class in 'α' by multiplying by the 'normUnit'. The 'normUnit' is the unit element associated with 'x' in the normalization monoid.
More concisely: For any cancel commutative monoid with additive identity 'α' having a normalization monoid structure, normalizing an element 'x' equals multiplying 'x' by its norm unit.
|
GCDMonoid.lcm_zero_left
theorem GCDMonoid.lcm_zero_left :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] (a : α), lcm 0 a = 0
This theorem, named `GCDMonoid.lcm_zero_left`, states that for any type `α` which is a GCDMonoid with cancelable commutative monoid with zero properties, the least common multiple (lcm) of `0` and any element `a` of type `α` is `0`. In other words, `0` is left-absorbing in the operation of least common multiple in the context of a GCDMonoid.
More concisely: In a GCDMonoid with cancelable commutative monoid and zero properties, the least common multiple of any element with 0 is 0.
|
lcm_dvd_iff
theorem lcm_dvd_iff :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c : α},
lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
This theorem, `lcm_dvd_iff`, states that for any type `α` that has an instance of `CancelCommMonoidWithZero` and `GCDMonoid`, and for any three elements `a`, `b`, `c` of that type, the lowest common multiple (lcm) of `a` and `b` divides `c` if and only if both `a` divides `c` and `b` divides `c`. In other words, it relates the divisibility of a number by the lcm of two other numbers to the divisibility of that number by each of those two numbers individually. This is a fundamental property within number theory.
More concisely: For elements `a`, `b`, `c` of a type with `CancelCommMonoidWithZero` and `GCDMonoid structures, lcm(a, b) | c if and only if a | c and b | c.` (Here, `|` denotes divisibility.)
|
lcm_comm
theorem lcm_comm :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
lcm a b = lcm b a
This theorem, `lcm_comm`, asserts that the least common multiple (LCM) operation in a cancellation commutative monoid with zero and a normalized GCD monoid is commutative. In other words, for any two elements `a` and `b` of a given type `α` that satisfies these algebraic structures, the LCM of `a` and `b` is the same as the LCM of `b` and `a`.
More concisely: In a cancellation commutative monoid with zero and a normalized GCD monoid, the least common multiple of elements `a` and `b` equals the least common multiple of `b` and `a`.
|
gcd_assoc
theorem gcd_assoc :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (m n k : α),
gcd (gcd m n) k = gcd m (gcd n k)
The theorem `gcd_assoc` states that for any type `α` that is a cancel commutative monoid with zero and a normalized GCD monoid, the greatest common divisor (gcd) operation is associative. In other words, for any three elements `m`, `n`, and `k` of type `α`, the gcd of `m` and `n` taken together and then taking the gcd with `k` is equal to the gcd of `m` with the gcd of `n` and `k`. In mathematical notation, this is equivalent to stating that `gcd(gcd(m, n), k) = gcd(m, gcd(n, k))`.
More concisely: For any cancel commutative monoid with zero and a normalized GCD monoid type `α`, the associativity of the greatest common divisor operation holds: `gcd(gcd(m, n), k) = gcd(m, gcd(n, k))`.
|
GCDMonoid.dvd_gcd
theorem GCDMonoid.dvd_gcd :
∀ {α : Type u_2} [inst : CancelCommMonoidWithZero α] [self : GCDMonoid α] {a b c : α},
a ∣ c → a ∣ b → a ∣ gcd c b
This theorem states that for any type `α` which is a GCD Monoid with a cancel commutative operation with zero, any element `a` which divides both `c` and `b` also divides the greatest common divisor (GCD) of `c` and `b`. In other words, if `a` is a common divisor of `c` and `b`, then `a` is a divisor of the GCD of these two elements.
More concisely: If `α` is a GCD monoid with cancel commutative operation and zero, then any common divisor `a` of `c` and `b` in `α` is a divisor of their greatest common divisor.
|
dvd_gcd_mul_of_dvd_mul
theorem dvd_gcd_mul_of_dvd_mul :
∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : GCDMonoid α] {m n k : α},
k ∣ m * n → k ∣ gcd k m * n
This theorem states that for any type `α` that is a cancel commutative monoid with zero and also a GCD monoid, and for any elements `m`, `n`, and `k` of this type, if `k` divides the product of `m` and `n`, then `k` also divides the product of the greatest common divisor of `k` and `m` with `n`. In mathematical terms, given $k$, $m$, $n$ in a GCD monoid, if $k$ divides $m*n$, then $k$ also divides $\gcd(k, m)*n$.
More concisely: If `α` is a cancel commutative monoid with zero and a GCD monoid, then for any `m`, `n`, and `k` in `α`, if `k` divides `m * n`, then `k` divides `gcd(k, m) * n`.
|