IsOfFinAddOrder.addOrderOf_pos
theorem IsOfFinAddOrder.addOrderOf_pos :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x → 0 < addOrderOf x
The theorem `IsOfFinAddOrder.addOrderOf_pos` states that for any additive monoid `G` and any element `x` of `G`, if `x` has a finite additive order (i.e., there exists a positive integer `n` such that `n` times `x` equals the additive identity), then the additive order of `x` (which is the smallest positive `n` that satisfies `n * x = 0`) is strictly greater than zero.
More concisely: For any additive monoid G and any element x with finite additive order, the additive order of x is a positive integer.
|
card_nsmul_eq_zero'
theorem card_nsmul_eq_zero' : ∀ {G : Type u_6} [inst : AddGroup G] {x : G}, Nat.card G • x = 0
The theorem `card_nsmul_eq_zero'` states that for any type `G` that forms an additive group, and for any element `x` in `G`, the cardinality of `G` times `x` equals zero. In other words, if we multiply `x` by the number of elements in `G` (or add `x` to itself that many times), we get the additive identity element, which is zero in the additive group. If `G` is infinite, its cardinality is defined as zero, so this theorem also holds for infinite groups.
More concisely: For any additive group G and element x in G, the product of the cardinality of G and x is zero.
|
not_isOfFinOrder_of_injective_pow
theorem not_isOfFinOrder_of_injective_pow :
∀ {G : Type u_1} [inst : Monoid G] {x : G}, (Function.Injective fun n => x ^ n) → ¬IsOfFinOrder x
This theorem states that for any element `x` of a monoid `G`, if the function that raises `x` to the power of `n` (for any n) is injective (meaning that for any two distinct integers `n` and `m`, `x^n` is different from `x^m`), then `x` cannot have finite order. In other words, there is no positive integer `n` such that raising `x` to the power `n` yields the identity element of the monoid.
More concisely: If the power function of an element in a monoid is injective, then the element has infinite order.
|
orderOf_dvd_of_pow_eq_one
theorem orderOf_dvd_of_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, x ^ n = 1 → orderOf x ∣ n := by
sorry
The theorem `orderOf_dvd_of_pow_eq_one` states that for any type `G` that is a monoid and any element `x` of `G`, if `x` raised to the power `n` equals 1 then the order of `x` divides `n`. Here, the order of `x` is the smallest positive integer `n` for which `x` to the power `n` equals 1, or 0 if no such integer exists (which indicates that `x` is of infinite order). In mathematical notation, if $x^n = 1$, then $orderOf\ x | n$.
More concisely: For any monoid `G` and its element `x`, if `x^n` equals 1 then the order of `x` divides `n`.
|
pow_eq_pow_iff_modEq
theorem pow_eq_pow_iff_modEq :
∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G} {m n : ℕ}, x ^ n = x ^ m ↔ (orderOf x).ModEq n m
This theorem named `pow_eq_pow_iff_modEq` states that for any type `G` that has an instance of `LeftCancelMonoid`, for any element `x` of `G`, and for any natural numbers `m` and `n`, the power of `x` raised to `n` equals the power of `x` raised to `m` if and only if `n` is congruent to `m` modulo the order of `x`. In other words, two exponents yield the same power of an element if and only if they are equivalent when divided by the order of the element, taking the remainder.
More concisely: For any element x of a left cancelable monoid G and natural numbers m and n, x^n = x^m if and only if n is congruent to m modulo the order of x.
|
IsOfFinOrder.of_inv
theorem IsOfFinOrder.of_inv : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x⁻¹ → IsOfFinOrder x
The theorem `IsOfFinOrder.of_inv` states that for any group `G` and any element `x` of that group, if the inverse of `x` has a finite order, then `x` itself also has a finite order. In the language of group theory, an element has a "finite order" if there exists a positive integer `n` such that raising the element to the power of `n` yields the identity element of the group. Therefore, this theorem essentially says that if `x⁻¹^n = 1` for some `n ≥ 1`, then `x^n = 1` for some `n ≥ 1` as well.
More concisely: If the inverse of an element in a group has finite order, then the element itself has finite order.
|
AddCommute.addOrderOf_add_dvd_lcm
theorem AddCommute.addOrderOf_add_dvd_lcm :
∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
AddCommute x y → addOrderOf (x + y) ∣ (addOrderOf x).lcm (addOrderOf y)
The theorem `AddCommute.addOrderOf_add_dvd_lcm` states that for any type `G` that has an additive monoid structure, given any two elements `x` and `y` of `G` that commute additively (that is, `x + y = y + x`), the additive order of `x + y` is a divisor of the least common multiple of the additive orders of `x` and `y`. In other words, if we denote by `n • a` the result of adding `a` to itself `n` times, the smallest number `n` such that `n • (x + y) = 0` divides the least common multiple of the smallest numbers `m` and `l` such that `m • x = 0` and `l • y = 0`, respectively.
More concisely: For any commuting additive monoid elements x and y, the additive order of x + y divides the least common multiple of the additive orders of x and y.
|
IsOfFinOrder.mem_powers_iff_mem_zpowers
theorem IsOfFinOrder.mem_powers_iff_mem_zpowers :
∀ {G : Type u_1} [inst : Group G] {x y : G}, IsOfFinOrder x → (y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x)
The theorem `IsOfFinOrder.mem_powers_iff_mem_zpowers` states that for any group `G` and any elements `x` and `y` of the group, if `x` is of finite order (meaning there exists a non-zero integer `n` such that `x` raised to the power of `n` equals the identity element), then `y` belongs to the submonoid generated by `x` if and only if `y` belongs to the subgroup generated by `x`. The submonoid generated by `x` is the set of all elements that can be obtained by multiplying `x` with itself some number of times, and the subgroup generated by `x` is the set of all elements that can be obtained by multiplying `x` or its inverse with itself some number of times.
More concisely: For any group `G` and elements `x` of finite order in `G`, `x` generates the same subgroup and submonoid, i.e., `y` is in the submonoid generated by `x` if and only if `y` is in the subgroup generated by `x`.
|
Commute.orderOf_mul_dvd_lcm
theorem Commute.orderOf_mul_dvd_lcm :
∀ {G : Type u_1} [inst : Monoid G] {x y : G}, Commute x y → orderOf (x * y) ∣ (orderOf x).lcm (orderOf y) := by
sorry
This theorem states that for any type `G` that has a monoid structure, given two elements `x` and `y` of `G` that commute (i.e., `x * y = y * x`), the order of the product `x * y` divides the least common multiple of the orders of `x` and `y`. Here, the order of an element `a` in a monoid is the smallest positive integer `n` such that `a^n = 1`, or zero if no such integer exists. The least common multiple of two natural numbers `m` and `n` is defined as the product of `m` and `n` divided by their greatest common divisor.
More concisely: For any commuting elements `x` and `y` in a monoid `G` with finite orders, the order of their product `x * y` divides their least common multiple.
|
card_nsmul_eq_zero
theorem card_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G}, Fintype.card G • x = 0
The theorem `card_nsmul_eq_zero` states that for any type `G` that has both an additive group structure and a finite type structure, and any element `x` of that type `G`, the finite cardinality of `G` (notated as `Fintype.card G`) times `x` (i.e., the element `x` added to itself `Fintype.card G` times) equals `0`. In other words, if you add an element to itself as many times as there are elements in the finite set, you will get the additive identity (zero).
More concisely: For any finite additive group `G` and its element `x`, we have `Fintype.card G * x = 0`.
|
addOrderOf_eq_zero_iff
theorem addOrderOf_eq_zero_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x = 0 ↔ ¬IsOfFinAddOrder x
The theorem `addOrderOf_eq_zero_iff` states that for any type `G` that is an additive monoid and any element `x` of type `G`, the additive order of `x` is zero if and only if `x` is not of finite additive order. In mathematical terms, if there does not exist a nonnegative integer `n` such that `n * x = 0`, then the additive order of `x` is defined to be zero. Conversely, if the additive order of `x` is zero, this indicates that `x` does not have a finite additive order.
More concisely: The additive order of an element in an additive monoid is zero if and only if the element has no finite additive order.
|
isOfFinAddOrder_of_finite
theorem isOfFinAddOrder_of_finite :
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G] (x : G), IsOfFinAddOrder x
The theorem `isOfFinAddOrder_of_finite` states that for any type `G`, given an additive left-cancelable monoid structure and a finiteness condition on `G`, any element `x` of `G` is of finite additive order. In other words, for every `x` in `G`, there exists a positive integer `n` such that `n • x = 0`. In this context, "left-cancelable" means that for all `a, b, c` in `G`, if `a + b = a + c`, then `b = c`.
More concisely: Given a type `G` equipped with an additive monoid structure and a finite element `x` in `G`, `x` has finite additive order.
|
isOfFinAddOrder_iff_nsmul_eq_zero
theorem isOfFinAddOrder_iff_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x ↔ ∃ n, 0 < n ∧ n • x = 0
This theorem states that, for any type `G` which has an additive monoid structure, an element `x` of `G` is of finite additive order if and only if there exists a positive integer `n` such that `n • x = 0`. This means that the element `x` is of finite additive order if it becomes zero when repeatedly added to itself `n` times for some positive integer `n`.
More concisely: For any additive monoid `G`, an element `x` in `G` has finite additive order if and only if there exists a positive integer `n` such that `x + ... + x = 0` (n times).
|
IsOfFinOrder.mul
theorem IsOfFinOrder.mul :
∀ {G : Type u_1} [inst : CommMonoid G] {x y : G}, IsOfFinOrder x → IsOfFinOrder y → IsOfFinOrder (x * y)
The theorem states that in a commutative monoid, the property of having finite order is closed under multiplication. Specifically, given any two elements `x` and `y` of the commutative monoid `G` that both have finite order, their product `x * y` also has finite order. Here, an element is said to have finite order if there exists a positive integer `n` such that raising the element to the power `n` gives the identity element `1`.
More concisely: In a commutative monoid, if every element has finite order, then the product of any two such elements also has finite order.
|
addOrderOf_eq_zero
theorem addOrderOf_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, ¬IsOfFinAddOrder x → addOrderOf x = 0 := by
sorry
The theorem `addOrderOf_eq_zero` states that for any type `G` that forms an additive monoid, for any element `x` of `G`, if `x` does not have finite additive order, then the additive order of `x` is zero. In other words, if there does not exist a non-zero natural number `n` such that `n` times `x` equals the zero element of the monoid, then the additive order of `x` is defined to be zero by convention.
More concisely: If an element in an additive monoid does not have a finite additive order, then its additive order is zero by convention.
|
orderOf_pow
theorem orderOf_pow :
∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G] {n : ℕ} (x : G),
orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
This theorem, `orderOf_pow`, states that for any type `G` that is a left cancelable monoid and finite, for any natural number `n`, and for any element `x` of type `G`, the order of `x` to the power of `n` is equal to the order of `x` divided by the greatest common divisor of the order of `x` and `n`. In simpler terms, raising an element of a finite cancelable monoid to a power changes the order of that element to the original order divided by the greatest common divisor of the original order and the exponent.
More concisely: For any finite, left cancelable monoid `G` and its element `x` with finite order, the order of `x` raised to the power `n` equals the order of `x` divided by the greatest common divisor of their orders.
|
not_isOfFinAddOrder_of_injective_nsmul
theorem not_isOfFinAddOrder_of_injective_nsmul :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, (Function.Injective fun n => n • x) → ¬IsOfFinAddOrder x
This theorem, `not_isOfFinAddOrder_of_injective_nsmul`, states that for any given type `G` equipped with an additive monoid structure, and any element `x` of `G`, if the function that multiplies `x` by an integer `n` is injective (i.e., distinct integers yield distinct multiples of `x`), then `x` cannot be of finite additive order. In other words, there does not exist a positive integer `n` such that `n` times `x` equals zero in the additive monoid `G`.
More concisely: If the multiplication by an element `x` of an additive monoid `G` is an injection, then `x` has no finite additive order in `G`.
|
AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd
theorem AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd :
∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
AddCommute x y →
IsOfFinAddOrder y →
(∀ (p : ℕ), p.Prime → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y) →
addOrderOf (x + y) = addOrderOf y
This theorem states that, given an additive monoid `G` and two elements `x` and `y` of `G` such that `x` and `y` commute (i.e., `a + b = b + a`), if `y` has finite order and every prime factor `p` of the order of `x` not only divides the order of `x` but also, when multiplied by the order of `x`, divides the order of `y`, then the order of the element `x + y` is equal to the order of `y`. Here, the order of an element `a` is defined as the smallest positive integer `n` such that `n • a = 0`, or `0` if no such `n` exists.
More concisely: If `x` and `y` are commuting elements of an additive monoid `G`, `y` has finite order, and every prime factor of the order of `x` that also divides the order of `y` when multiplied by the order of `x` also divides the order of `y`, then the order of `x + y` equals the order of `y`.
|
IsOfFinOrder.inv
theorem IsOfFinOrder.inv : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x → IsOfFinOrder x⁻¹
This theorem, `IsOfFinOrder.inv`, states that in any group `G`, if an element `x` has finite order, then its inverse `x⁻¹` also has finite order. In other words, if there exists a positive integer `n` such that `x^n = 1`, then there also exists a positive integer (possibly different from `n`) such that `(x⁻¹)^n = 1`.
More concisely: If an element in a group has finite order, then its inverse also has finite order with the same order or some other finite order.
|
isOfFinOrder_of_finite
theorem isOfFinOrder_of_finite :
∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G] (x : G), IsOfFinOrder x
This theorem states that for any type `G`, given that `G` is a Left Cancelable Monoid and `G` is finite, every element `x` of `G` is of finite order. Here, an element `x` of `G` being of finite order means that there exists a positive integer `n` such that raising `x` to the power `n` equals the identity of the monoid, i.e., `x ^ n = 1`. A Left Cancelable Monoid is a monoid (an algebraic structure equipped with an associative binary operation and an identity element) with the additional property that for all elements `a`, `b`, and `c`, if `a * b = a * c`, then `b = c`. A finite `G` means that the type `G` has a finite number of elements.
More concisely: In a finite, left cancelable monoid, every non-identity element has finite order.
|
IsOfFinAddOrder.add
theorem IsOfFinAddOrder.add :
∀ {G : Type u_1} [inst : AddCommMonoid G] {x y : G},
IsOfFinAddOrder x → IsOfFinAddOrder y → IsOfFinAddOrder (x + y)
This theorem states that the property of having finite additive order is preserved under addition. More specifically, for any type `G` that forms a commutative additive monoid, if two elements `x` and `y` of `G` both have finite additive order, then their sum `x + y` will also have finite additive order. Here, an element having finite additive order means that there exists a non-zero integer `n` such that adding the element to itself `n` times results in the zero of the monoid.
More concisely: If `G` is a commutative additive monoid and `x` and `y` are elements of `G` with finite additive orders, then `x + y` also has finite additive order.
|
Mathlib.GroupTheory.OrderOfElement._auxLemma.4
theorem Mathlib.GroupTheory.OrderOfElement._auxLemma.4 :
∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) = ∀ (x : α), ¬p x
This theorem states that for any property `p` that can be assigned to elements `x` of a type `α`, the statement "there does not exist an element `x` for which the property `p` holds" is equivalent to the statement "for all elements `x`, the property `p` does not hold". In other words, there is no `x` such that `p(x)` is true if and only if `p(x)` is false for every `x`.
More concisely: The negation of "there exists an x : α such that p(x) holds" is equivalent to "for all x : α, not p(x) holds".
|
addOrderOf_nsmul
theorem addOrderOf_nsmul :
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G] {n : ℕ} (x : G),
addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
The theorem `addOrderOf_nsmul` states that for any type 'G' that has the structure of a finite left-cancelable additive monoid, for any natural number 'n' and any element 'x' of 'G', the additive order of 'n' times 'x' is equal to the additive order of 'x' divided by the greatest common divisor of the additive order of 'x' and 'n'. Here, the additive order of an element 'a' is the smallest natural number 'n' such that 'n' times 'a' equals zero, or zero if no such 'n' exists (indicating that 'a' has infinite order).
More concisely: For any finite left-cancelable additive monoid 'G' and any 'x' in 'G' and natural number 'n', the additive order of 'n' × 'x' equals the greatest common divisor of the additive orders of 'x' and 'n'.
|
AddSubmonoid.isOfFinAddOrder_coe
theorem AddSubmonoid.isOfFinAddOrder_coe :
∀ {G : Type u_1} [inst : AddMonoid G] {H : AddSubmonoid G} {x : ↥H}, IsOfFinAddOrder ↑x ↔ IsOfFinAddOrder x := by
sorry
The theorem `AddSubmonoid.isOfFinAddOrder_coe` states that for any additive monoid `G` and any additive submonoid `H` of `G`, an element `x` of `H` is of finite order in `G` if and only if it is of finite order in `H`. In other words, there exists a natural number `n ≥ 1` such that `n • x = 0` in `G` if and only if the same condition holds in `H`.
More concisely: An element of finite order in an additive submonoid of a commutative additive monoid is of finite order in the monoid with the same order.
|
IsOfFinOrder.apply
theorem IsOfFinOrder.apply :
∀ {η : Type u_6} {Gs : η → Type u_7} [inst : (i : η) → Monoid (Gs i)] {x : (i : η) → Gs i},
IsOfFinOrder x → ∀ (i : η), IsOfFinOrder (x i)
This theorem states that if a direct product of monoids has finite order, then each individual component of the product must also have finite order. In other words, if for some element `x`, which is a function mapping to each one of the monoids, `x` has finite order (meaning there exists a positive integer `n` such that `x^n = 1`), then for any `i`, the element `x(i)` of the monoid `Gs(i)` also has finite order.
More concisely: If a direct product of monoids has finite order, then each component monoid has an element of finite order.
|
pow_card_eq_one
theorem pow_card_eq_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, x ^ Fintype.card G = 1 := by
sorry
The theorem `pow_card_eq_one` states that for any finite group `G` and any element `x` of `G`, the element `x` raised to the power of the cardinality (or size) of `G` (denoted by `Fintype.card G`) equals the group's identity element. In mathematical terms, given a finite group `G` with `n` elements (where `n` is the number of elements in `G`), for all `x` in `G`, `x^n = 1`, where `1` is the identity element in `G`.
More concisely: For any finite group G and any of its elements x, x raised to the power of the group's cardinality equals the identity element. (x^(Fintype.card G) = 1)
|
isOfFinOrder_inv_iff
theorem isOfFinOrder_inv_iff : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x
The theorem `isOfFinOrder_inv_iff` states that for any type `G` that is a group and any element `x` of `G`, the inverse of `x` has finite order if and only if `x` itself has finite order. Here, an element having finite order means that there exists some non-zero positive integer `n` such that when the element is raised to the power of `n`, the result is the identity element of the group.
More concisely: For any group `G` and its element `x`, `x` and its inverse have finite orders if and only if each other.
|
addOrderOf_dvd_iff_nsmul_eq_zero
theorem addOrderOf_dvd_iff_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, addOrderOf x ∣ n ↔ n • x = 0
The theorem `addOrderOf_dvd_iff_nsmul_eq_zero` states that for any type `G` which is an instance of `AddMonoid`, for any element `x` of `G` and any natural number `n`, the order of `x` (as defined by the function `addOrderOf`) divides `n` if and only if `n` times `x` equals the additive identity (i.e., `0`). In other words, if `n` is a multiple of `x`'s order, then `n`-fold sum of `x` results in the additive identity, and conversely, if `n`-fold sum of `x` is the additive identity, then `n` is a multiple of `x`'s order.
More concisely: For any AddMonoid type G and its element x, the order of x divides natural number n if and only if n * x = 0.
|
orderOf_units
theorem orderOf_units : ∀ {G : Type u_1} [inst : Monoid G] {y : Gˣ}, orderOf ↑y = orderOf y
The theorem `orderOf_units` states that for any type `G` that is a monoid, and for any unit element `y` of `G` (denoted as `Gˣ`), the order of the coerced unit element `↑y` (which means `y` is viewed as an element of `G`) is equal to the order of `y`. In other words, the order of a unit element remains the same even when it's considered as an element of the monoid.
More concisely: For any monoid `G` and unit `y` in `G`, the order of the unit `y` is equal to the order of the coerced unit `↑y` in `G`.
|
mod_addOrderOf_nsmul
theorem mod_addOrderOf_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G) (n : ℕ), (n % addOrderOf x) • x = n • x
This theorem, `mod_addOrderOf_nsmul`, states that for all types `G` which are additively structured as a monoid and for any element `x` of `G` and natural number `n`, the `n`th multiple of `x` is equal to the multiple of `x` by the remainder when `n` is divided by `addOrderOf x`. Here, `addOrderOf x` represents the order of element `x`, which is the smallest positive integer `n` such that `n * x = 0`, or `0` if `x` has infinite order. The theorem essentially describes a property of periodicity in the context of additive monoids.
More concisely: For any additively structured monoid type `G` and element `x` of `G` with order `n`, the `n`th multiple of `x` equals the `n`th power of `x` modulo the order of `x`.
|
isOfFinOrder_one
theorem isOfFinOrder_one : ∀ {G : Type u_1} [inst : Monoid G], IsOfFinOrder 1
This theorem states that the element 1 is of finite order in any monoid. In other words, for any given monoid, there exists a positive integer `n` such that raising 1 to the power of `n` results in 1. This is a universal property that holds for the identity element in all monoids.
More concisely: In any monoid, the identity element has finite order for some positive integer.
|
orderOf_eq_one_iff
theorem orderOf_eq_one_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x = 1 ↔ x = 1
The theorem `orderOf_eq_one_iff` asserts that for any type `G` equipped with a monoid structure, and any element `x` of `G`, the order of `x` is equal to `1` if and only if `x` itself is the identity element of the monoid. In other words, in the context of a monoid, an element has order `1` exactly when it is the identity element.
More concisely: For any monoid `G` and its identity element `e`, the order of `e` is equal to 1 if and only if `e` is the identity element itself.
|
addOrderOf_dvd_card
theorem addOrderOf_dvd_card :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G}, addOrderOf x ∣ Fintype.card G
This theorem states that for any finite additive group `G` and any element `x` in `G`, the order of the element `x` (denoted by `addOrderOf x`) divides the cardinality of the group `G` (denoted by `Fintype.card G`). In the context of group theory, the order of an element is the smallest positive integer such that the element, when added to itself that many times, results in the additive identity (usually zero). The cardinality of a group is just the number of elements in the group. Therefore, this theorem is a statement about the relationship between the order of an element and the size of the group it belongs to.
More concisely: For any finite additive group `G` and its element `x`, the order of `x` divides the cardinality of `G`.
|
Mathlib.GroupTheory.OrderOfElement._auxLemma.8
theorem Mathlib.GroupTheory.OrderOfElement._auxLemma.8 :
∀ {G : Type u_1} [inst : Monoid G] {x : G}, (orderOf x = 1) = (x = 1)
This theorem states that for any type `G` that has a `Monoid` structure, and for any element `x` of type `G`, the order of `x` equals `1` if and only if `x` itself equals the identity `1`. Here the order of an element `x`, denoted by `orderOf x`, corresponds to the smallest natural number `n ≥ 1` such that `x` to the power `n` equals `1`. If no such `n` exists (i.e., if `x` is of infinite order), `orderOf x` is defined to be `0`.
More concisely: For any monoid `G` and element `x` in `G`, the order of `x` equals 1 if and only if `x` is the identity element of `G`.
|
orderOf_eq_of_pow_and_pow_div_prime
theorem orderOf_eq_of_pow_and_pow_div_prime :
∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ},
0 < n → x ^ n = 1 → (∀ (p : ℕ), p.Prime → p ∣ n → x ^ (n / p) ≠ 1) → orderOf x = n
The theorem `orderOf_eq_of_pow_and_pow_div_prime` states the following:
For a given monoid `G`, let's consider an element `x` of `G` and a positive natural number `n`. If `x` raised to the power `n` equals the identity element of `G` (i.e., `x^n = 1`) and for all prime numbers `p` that divide `n`, `x` raised to the power `n/p` does not equal the identity (i.e., `x^(n/p) ≠ 1`), then the order of element `x` in `G` is `n`.
In simpler terms, in a monoid, if an element to a power gives us the identity and to all smaller powers (obtained by dividing the original power by any of its prime factors) it does not, then the original power is indeed the order of this element in the monoid.
More concisely: If an element `x` in a monoid `G` satisfies `x^n = 1` and `x^(n/p) ≠ 1` for all prime factors `p` of `n`, then the order of `x` in `G` is `n`.
|
Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd
theorem Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd :
∀ {G : Type u_1} [inst : Monoid G] {x y : G},
Commute x y →
IsOfFinOrder y →
(∀ (p : ℕ), p.Prime → p ∣ orderOf x → p * orderOf x ∣ orderOf y) → orderOf (x * y) = orderOf y
This theorem states that in a monoid, if each prime factor of the order of an element 'x' appears with higher multiplicity in the order of another element 'y', and 'x' commutes with 'y', then the order of the product 'x * y' is the same as the order of 'y'. Here, the order of an element is the minimum positive integer 'n' such that the element raised to the power 'n' equals the identity, and a number is called a prime if it's not zero, not a unit, and if it divides the product of two numbers, then it divides at least one of them.
More concisely: In a monoid, if the order of element $x$ is divisible by the power of each prime factor that appears with higher multiplicity in the order of element $y$, and $x$ commutes with $y$, then the order of $xy$ equals the order of $y$.
|
orderOf_injective
theorem orderOf_injective :
∀ {G : Type u_1} [inst : Monoid G] {H : Type u_6} [inst_1 : Monoid H] (f : G →* H),
Function.Injective ⇑f → ∀ (x : G), orderOf (f x) = orderOf x
The theorem `orderOf_injective` states that for any two types `G` and `H` that are both monoids, if there exists a monoid homomorphism `f` from `G` to `H` that is injective, then for any element `x` of `G`, the order of `f(x)` in `H` is equal to the order of `x` in `G`.
In other words, an injective monoid homomorphism preserves the order of elements. Here, the order of an element is the smallest positive integer `n` such that `x^n = 1`, or `0` if no such `n` exists (meaning that `x` is of infinite order).
More concisely: If `f` is an injective monoid homomorphism from monoid `G` to monoid `H`, then for all `x` in `G`, the order of `x` in `G` equals the order of `f(x)` in `H`.
|
Nat.card_addSubmonoidMultiples
theorem Nat.card_addSubmonoidMultiples :
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {a : G}, Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a := by
sorry
The theorem `Nat.card_addSubmonoidMultiples` states that for any type `G` that forms an `AddLeftCancelMonoid`, and any element `a` of `G`, the cardinality of the additive submonoid generated by `a` (i.e., the set of all multiples of `a`) is equal to the additive order of `a`. The additive order of `a` is the least positive integer `n` such that `n` times `a` equals zero, or `0` if `a` has infinite order.
More concisely: The cardinality of the additive submonoid generated by an element `a` in an add left cancel monoid `G` equals the additive order of `a`.
|
exists_pow_eq_self_of_coprime
theorem exists_pow_eq_self_of_coprime :
∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, n.Coprime (orderOf x) → ∃ m, (x ^ n) ^ m = x
The theorem "exists_pow_eq_self_of_coprime" states that for any type `G` that forms a Monoid, any element `x` of this Monoid, and any natural number `n` such that `n` and the order of `x` are coprime (their greatest common divisor is 1), there exists a natural number `m` such that raising `x` to the power of `n` and then to the power of `m` gives `x` back. In mathematical notation, if gcd(`n`, order(`x`)) = 1, then there exists `m` such that `(x^n)^m = x`.
More concisely: For any Monoid `G` and element `x` of `G` with coprime order `n`, there exists a natural number `m` such that `x^(nm) = x`.
|
Mathlib.GroupTheory.OrderOfElement._auxLemma.5
theorem Mathlib.GroupTheory.OrderOfElement._auxLemma.5 : ∀ {a b : Prop}, (¬(a ∧ b)) = (a → ¬b)
This theorem, in the context of group theory and order of elements, states that for any two propositions 'a' and 'b', the negation of the conjunction of 'a' and 'b' (not (a and b)) is logically equivalent to the implication that if 'a' is true, then 'b' must be false (a implies not b).
In other words, it says that it's not possible for both 'a' and 'b' to be true at the same time if and only if the truth of 'a' guarantees the falsity of 'b'.
More concisely: The negation of the conjunction of propositions 'a' and 'b' is logically equivalent to the implication 'a → ¬b'.
|
orderOf_eq_zero
theorem orderOf_eq_zero : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, ¬IsOfFinOrder x → orderOf x = 0
The theorem `orderOf_eq_zero` states that for any type `G` that forms a monoid, and any element `x` of type `G`, if `x` is not of finite order (meaning, there doesn't exist a positive natural number `n` such that `x` raised to the power `n` equals the identity element), then the order of `x` is zero. In other words, if an element of a monoid does not have a finite order, its order by convention is zero.
More concisely: If a monoid element has no finite order, then its order is 0.
|
Mathlib.GroupTheory.OrderOfElement._auxLemma.3
theorem Mathlib.GroupTheory.OrderOfElement._auxLemma.3 :
∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x = ∃ n, 0 < n ∧ x ^ n = 1
The theorem, named `Mathlib.GroupTheory.OrderOfElement._auxLemma.3`, states that for any type `G` which forms a Monoid, an element `x` of `G` is of finite order (i.e., `IsOfFinOrder x`) if and only if there exists a positive integer `n` such that raising `x` to the power of `n` equals the identity element of the Monoid (`1`). In mathematical notation, this can be written as: $x^n = 1$. This theorem relates the notion of finite order to the existence of an exponent that brings the element to the identity.
More concisely: For any monoid `G` and element `x` in `G`, `x` has finite order if and only if there exists a positive integer `n` such that `x^n = 1`.
|
IsOfFinAddOrder.apply
theorem IsOfFinAddOrder.apply :
∀ {η : Type u_6} {Gs : η → Type u_7} [inst : (i : η) → AddMonoid (Gs i)] {x : (i : η) → Gs i},
IsOfFinAddOrder x → ∀ (i : η), IsOfFinAddOrder (x i)
The theorem `IsOfFinAddOrder.apply` states that, given a direct product of additive monoids, if the direct product has finite additive order then each individual component also has finite additive order. More specifically, for each element `x` of the direct product, if `x` satisfies that there exists a non-negative integer `n` such that `n • x = 0` (which is the definition of `IsOfFinAddOrder`), then for each individual component `i`, `x i` also satisfies the same property. In other words, the finite additive order property is preserved by the projection to each component of the direct product.
More concisely: If a direct product of additive monoids has finite additive order, then each component monoid also has an element of finite additive order with the same order.
|
addOrderOf_zero
theorem addOrderOf_zero : ∀ {G : Type u_1} [inst : AddMonoid G], addOrderOf 0 = 1
This theorem states that for any type `G` that forms an additive monoid, the additive order of the element `0` is `1`. In mathematical terms, this means that the smallest positive natural number `n` such that `n * 0 = 0` (where `*` denotes the multiplication operation in the monoid) is `1`. Remember that the additive order of an element in an additive monoid is the smallest positive integer that results in the additive identity when the element is repeatedly added to itself that many times. In this case, `0` added to itself any number of times will always result in `0`, and thus its additive order is `1`.
More concisely: For any additive monoid `G` with identity element `0`, the additive order of `0` is 1.
|
pow_orderOf_eq_one
theorem pow_orderOf_eq_one : ∀ {G : Type u_1} [inst : Monoid G] (x : G), x ^ orderOf x = 1
The theorem `pow_orderOf_eq_one` states that for any type `G` that is a monoid, and for every element `x` from this monoid, when `x` is raised to the power of its order (`orderOf x`), the result will be the identity element of the monoid, which is `1`. In other words, in any monoid, raising an element to the power of its order always yields the monoid's identity.
More concisely: For any monoid `G` and element `x` in `G`, `x^(orderOf x) = 1`.
|
IsOfFinAddOrder.addOrderOf_nsmul
theorem IsOfFinAddOrder.addOrderOf_nsmul :
∀ {G : Type u_1} [inst : AddMonoid G] (x : G) (n : ℕ),
IsOfFinAddOrder x → addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
The theorem "IsOfFinAddOrder.addOrderOf_nsmul" states that for any type `G` that has a structure of an additive monoid and for any element `x` of `G` which has a finite additive order, and any natural number `n`, the order of the element `n • x` equals the order of `x` divided by the greatest common divisor of the order of `x` and `n`. Here, the order of an element is defined as the smallest positive integer such that multiplying the element by that integer results in the additive identity (zero), and if no such integer exists, the order is conventionally set to zero. The order of multiplication by `n` is the smallest number of applications required to get zero.
More concisely: For any element `x` of an additive monoid `G` with finite additive order, the order of `n • x` equals the greatest common divisor of the orders of `x` and `n`.
|
isOfFinAddOrder_zero
theorem isOfFinAddOrder_zero : ∀ {G : Type u_1} [inst : AddMonoid G], IsOfFinAddOrder 0
The theorem `isOfFinAddOrder_zero` states that the element 0 has finite order in any additive monoid. In other words, for any type `G` that has an additive monoid structure, there exists a positive integer `n` such that adding 0 to itself `n` times results in 0. This is true because the sum of zero with itself any number of times is always zero.
More concisely: For any additive monoid, there exists a positive integer `n` such that adding its identity element (0) to itself `n` times equals the identity element.
|
Fintype.card_zpowers
theorem Fintype.card_zpowers :
∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, Fintype.card ↥(Subgroup.zpowers x) = orderOf x := by
sorry
The theorem `Fintype.card_zpowers` states that for any group `G` that is also a finite type and any element `x` of `G`, the number of elements in the subgroup generated by `x` is equal to the order of `x`. In mathematical terms, if `G` is a group and `x` is an element of `G`, the size (or cardinality) of the subgroup of `G` generated by the powers of `x` is equal to the smallest positive integer `n` such that `x^n = 1` (this `n` is called the order of `x`). If no such `n` exists, which means `x` has infinite order, then by convention, the order of `x` is defined to be `0`, and this theorem states that the subgroup generated by `x` is infinite.
More concisely: The order of a finite group element equals the cardinality of the subgroup generated by its powers.
|
addOrderOf_nsmul_eq_zero
theorem addOrderOf_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G), addOrderOf x • x = 0
The theorem `addOrderOf_nsmul_eq_zero` states that for any type `G` that has an `AddMonoid` structure, for any element `x` of `G`, the `addOrderOf` of `x` (denoted as `n`) times the scalar multiplication of `x` is equal to zero. In other words, if `n` is defined as the order of the element `x` (the smallest positive integer such that `n` times `x` equals zero, or zero if `x` has infinite order), then `n` times `x` is indeed zero.
More concisely: For any AddMonoid type G and element x of G with order n, n * x = 0.
|
addOrderOf_dvd_natCard
theorem addOrderOf_dvd_natCard : ∀ {G : Type u_6} [inst : AddGroup G] (x : G), addOrderOf x ∣ Nat.card G
The theorem `addOrderOf_dvd_natCard` states that for any type `G` that is an additive group, for every element `x` in `G`, the additive order of `x` divides the cardinality of `G` as a natural number. In other words, if `n` is the minimum positive number such that adding `x` to itself `n` times results in the additive identity (or if `x` has infinite order, `n` is defined to be `0`), then `n` is a divisor of the number of elements in `G`. If `G` is infinite, its cardinality is defined to be `0`.
More concisely: For any additive group G and every x in G, the order of x as an element of G divides the cardinality of G as natural numbers.
|
addOrderOf_eq_of_nsmul_and_div_prime_nsmul
theorem addOrderOf_eq_of_nsmul_and_div_prime_nsmul :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ},
0 < n → n • x = 0 → (∀ (p : ℕ), p.Prime → p ∣ n → (n / p) • x ≠ 0) → addOrderOf x = n
This theorem states that for any element `x` of an additive monoid `G` and any positive natural number `n`, if `n` times `x` equals 0, and `n` divided by any prime factor `p` of `n` times `x` does not equal 0, then the order of `x` in `G` is `n`. Here, the order of an element is the smallest positive natural number `n` such that `n` times the element equals 0, or if no such `n` exists, the order is defined as 0. Furthermore, a prime number is defined as a number that is not 0, not a unit, and if it divides the product of any two numbers, it must divide at least one of them.
More concisely: If an element `x` of an additive monoid `G` satisfies `n * x = 0` and `p | n` implies `p * x != 0` for all prime factors `p` of `n`, then the order of `x` in `G` is equal to `n`.
|
isOfFinAddOrder_neg_iff
theorem isOfFinAddOrder_neg_iff :
∀ {G : Type u_1} [inst : AddGroup G] {x : G}, IsOfFinAddOrder (-x) ↔ IsOfFinAddOrder x
The theorem states that for any type `G` which is equipped with an additive group structure, an element `x` of `G` has finite additive order if and only if its additive inverse `-x` also has finite additive order. Here, an element having finite additive order means that there exists a non-zero natural number `n` such that adding the element to itself `n` times results in the additive identity (usually denoted by `0`).
More concisely: For any additive group `G` and element `x` in `G`, `x` has finite additive order if and only if `-x` has finite additive order.
|
AddCommute.isOfFinAddOrder_add
theorem AddCommute.isOfFinAddOrder_add :
∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
AddCommute x y → IsOfFinAddOrder x → IsOfFinAddOrder y → IsOfFinAddOrder (x + y)
This theorem states that for any additive monoid `G`, if `x` and `y` are elements of `G` that commute additively and both have finite additive order, then their sum `x + y` also has finite additive order. In mathematical terms, this means that if `a + b = b + a` and there exist positive integers `n` and `m` such that `n * a = 0` and `m * b = 0`, then there also exists a positive integer `p` such that `p * (a + b) = 0`.
More concisely: Given an additive monoid `G` and elements `x, y ∈ G` with finite additive orders `n` for `x` and `m` for `y`, such that `x` and `y` commute additively (`x + y = y + x`), there exists a positive integer `p` such that `p * (x + y) = 0`.
|
addOrderOf_le_of_nsmul_eq_zero
theorem addOrderOf_le_of_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, 0 < n → n • x = 0 → addOrderOf x ≤ n
The theorem `addOrderOf_le_of_nsmul_eq_zero` states that for any type `G` that is an instance of the `AddMonoid` typeclass, for any element `x` of `G`, and for any natural number `n` greater than `0`, if `n` times `x` equals `0`, then the additive order of `x` is less than or equal to `n`. The additive order of an element `x` in `G` is the smallest positive natural number `n` such that `n • x = 0`, or `0` if no such `n` exists (indicating that `x` has infinite order).
More concisely: For any AddMonoid type `G` and element `x` in `G`, if `x` has order at most `n` (i.e., `n * x = 0`), then the additive order of `x` is less than or equal to `n`.
|
addOrderOf_injective
theorem addOrderOf_injective :
∀ {G : Type u_1} [inst : AddMonoid G] {H : Type u_6} [inst_1 : AddMonoid H] (f : G →+ H),
Function.Injective ⇑f → ∀ (x : G), addOrderOf (f x) = addOrderOf x
The theorem `addOrderOf_injective` asserts that for any two types `G` and `H`, each equipped with an additive monoid structure, and any injective function `f` from type `G` to type `H` that preserves the additive monoid structure, the order of an element `x` of type `G` under addition (i.e., the smallest non-zero natural number `n` such that `n` times `x` equals zero, or zero if no such `n` exists) is the same as the order of the image of `x` under `f`. In other words, the injective function preserves the additive order of elements.
More concisely: If `f` is an injective function between additive monoids `G` and `H`, then for all `x` in `G`, the order of `x` under addition in `G` equals the order of `f(x)` under addition in `H`.
|
nsmul_eq_nsmul_iff_modEq
theorem nsmul_eq_nsmul_iff_modEq :
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G} {m n : ℕ}, n • x = m • x ↔ (addOrderOf x).ModEq n m := by
sorry
This theorem states that for any type `G` which is an additive left cancelable monoid, and given any element `x` of `G` and any two natural numbers `m` and `n`, `n` times operation `x` equals `m` times operation `x` if and only if `n` is congruent to `m` modulo the additive order of `x`. The additive order of `x` is the smallest positive natural number `n` such that `n` times operation `x` results in the additive identity (usually denoted as `0`), or it is `0` if `x` has an infinite order. An additive left cancelable monoid is a set equipped with an associative addition operation and an additive identity, which also has the property that for any three elements `a`, `b`, and `c` in the set, if `a + b = a + c`, then `b = c`.
More concisely: For any additive left cancelable monoid `G` and element `x` of `G`, the equality of `nx` and `mx` in `G` holds if and only if `n` is congruent to `m` modulo the additive order of `x`.
|
Submonoid.isOfFinOrder_coe
theorem Submonoid.isOfFinOrder_coe :
∀ {G : Type u_1} [inst : Monoid G] {H : Submonoid G} {x : ↥H}, IsOfFinOrder ↑x ↔ IsOfFinOrder x
This theorem states that if an element has finite order in the original monoid, it also has finite order when considered as an element of any submonoid of the original monoid, and vice versa. In other words, for any monoid `G`, its submonoid `H`, and an element `x` of `H`, `x` has finite order in `G` if and only if `x` has finite order in `H`. Here, an element `x` of a monoid is said to have finite order if there exists a positive integer `n` such that `x` raised to the power of `n` equals the identity element of the monoid.
More concisely: If `x` has finite order in monoid `G` if and only if `x` has finite order in any submonoid of `G`.
|
IsOfFinOrder.exists_pow_eq_one
theorem IsOfFinOrder.exists_pow_eq_one :
∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x → ∃ n, 0 < n ∧ x ^ n = 1
This theorem, **Alias of the forward direction of `isOfFinOrder_iff_pow_eq_one`**, states that for any type `G` which forms a monoid, and any element `x` of `G` that satisfies the predicate `IsOfFinOrder`, there exists a natural number `n` greater than 0 such that raising `x` to the power of `n` equals the identity element of the monoid. In other words, if `x` has finite order in the monoid, then there's a positive integer `n` such that `x` to the power `n` is the identity.
More concisely: For any monoid `G` and element `x` of finite order in `G`, there exists a positive integer `n` such that `x^n = 1_G`, where `1_G` is the identity element of `G`.
|
isPeriodicPt_add_iff_nsmul_eq_zero
theorem isPeriodicPt_add_iff_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {n : ℕ} (x : G), Function.IsPeriodicPt (fun x_1 => x + x_1) n 0 ↔ n • x = 0
The theorem `isPeriodicPt_add_iff_nsmul_eq_zero` states that for any type `G` which has an `AddMonoid` structure, and any natural number `n` and element `x` of type `G`, the function defined as `λ x_1 => x + x_1` is periodic at `0` with period `n` if and only if the `n`-fold addition of `x` (denoted by `n • x`) equals `0`. This theorem draws a connection between the periodicity of the function and the repetitive addition of an element in an additive monoid.
More concisely: For any additive monoid (G, +) and natural number n, an element x in G is periodic with period n under the addition operation if and only if n * x = 0.
|
orderOf_eq_prime
theorem orderOf_eq_prime :
∀ {G : Type u_1} [inst : Monoid G] {x : G} {p : ℕ} [hp : Fact p.Prime], x ^ p = 1 → x ≠ 1 → orderOf x = p := by
sorry
The theorem `orderOf_eq_prime` states that for any type `G` equipped with a monoid structure, any element `x` of `G`, and any natural number `p` which is a prime number, if `x` raised to the power `p` equals `1` and `x` is not equal to `1`, then the order of `x` is `p`. In mathematical terms, if $x^p = 1$ for a prime $p$ and $x \neq 1$, then the smallest positive number $n$ such that $x^n = 1$ is $p$.
More concisely: For any monoid `G` and `x` in `G` with order `p` being a prime number, if `x^p = 1` and `x ≠ 1`, then the order of `x` equals `p`.
|
Fintype.card_zmultiples
theorem Fintype.card_zmultiples :
∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G},
Fintype.card ↥(AddSubgroup.zmultiples x) = addOrderOf x
This theorem states that for any additive group `G` that is also a finite type, and for any element `x` of `G`, the cardinality of the subgroup generated by `x` (also known as `zmultiples` of `x`) is equal to the order of the element `x`. Here, the order of `x` (defined by `addOrderOf x`) is the smallest positive integer `n` such that `n` times `x` equals to the identity element of the group (0 in the case of additive groups), or is defined to be `0` if `x` has infinite order.
More concisely: For any finite additive group G and its element x, the cardinality of the subgroup generated by x equals the order of x.
|
Mathlib.GroupTheory.OrderOfElement._auxAddLemma.3
theorem Mathlib.GroupTheory.OrderOfElement._auxAddLemma.3 :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x = ∃ n, 0 < n ∧ n • x = 0
This theorem states that for any type `G` that forms an additive monoid, an element `x` of `G` is of finite additive order if and only if there exists a positive integer `n` such that the `n`-fold sum (or `n` "copies") of `x` equals the additive identity (zero). In other words, an element `x` in an additive monoid `G` is of finite order when it satisfies the property that for some positive `n`, `n • x = 0`, where `•` denotes repeated addition.
More concisely: An element in an additive monoid has finite order if and only if there exists a positive integer n such that the sum of n copies of the element equals the additive identity.
|
IsOfFinAddOrder.exists_nsmul_eq_zero
theorem IsOfFinAddOrder.exists_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x → ∃ n, 0 < n ∧ n • x = 0
The theorem `IsOfFinAddOrder.exists_nsmul_eq_zero` states that for any element `x` of an additive monoid `G` that satisfies the property `IsOfFinAddOrder`, there exists a positive integer `n` such that `n` multiplied by `x` (denoted as `n • x` in Lean) equals zero. In other words, if an element of an additive monoid has finite order, then there exists a non-zero multiple of this element that equals the additive identity (zero).
More concisely: For every additive monoid element `x` with finite order, there exists a positive integer `n` such that `n` times `x` equals the additive identity.
|
orderOf_le_of_pow_eq_one
theorem orderOf_le_of_pow_eq_one :
∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, 0 < n → x ^ n = 1 → orderOf x ≤ n
The theorem `orderOf_le_of_pow_eq_one` states that for any type `G` that forms a Monoid, and any element `x` in `G`, if there exists a natural number `n` greater than `0` such that raising `x` to the power `n` yields the identity `1`, then the order of `x` is less than or equal to `n`. In other words, if `x` to the power of `n` equals `1`, then `n` is at least as large as the smallest positive integer for which this is true, which is the order of `x`.
More concisely: If for some Monoid `G` and its element `x` there exists a natural number `n` such that `x^n = 1`, then the order of `x` is less than or equal to `n`.
|
orderOf_dvd_natCard
theorem orderOf_dvd_natCard : ∀ {G : Type u_6} [inst : Group G] (x : G), orderOf x ∣ Nat.card G
The theorem `orderOf_dvd_natCard` states that for any group `G` and for any element `x` in `G`, the order of `x` divides the cardinality of `G`. Here, the order of an element `x` in `G`, denoted as `orderOf x`, is the smallest positive integer `n` such that `x^n = 1`, or `0` if such an integer does not exist (meaning `x` has infinite order). The cardinality of `G`, denoted as `Nat.card G`, is the size of the set of elements in `G` translated into a natural number, or `0` if `G` is infinite. So this theorem is essentially a statement of Lagrange's theorem in group theory, which says that the order of any element divides the order of the group.
More concisely: For any group G and any of its elements x, the order of x divides the cardinality of G.
|
IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples
theorem IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples :
∀ {G : Type u_1} [inst : AddGroup G] {x y : G},
IsOfFinAddOrder x → (y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x)
This theorem states that for any additive group `G` and any two elements `x` and `y` of `G`, if `x` has a finite additive order (meaning that there exists a non-zero integer `n` such that `n * x = 0`), then `y` is in the additive submonoid generated by `x` if and only if `y` is in the additive subgroup generated by `x`. In other words, when `x` has finite order, the set of all multiples of `x` that form a submonoid is exactly the same as the set of all multiples of `x` that form a subgroup.
More concisely: For any additive group `G` and elements `x` and `y` of `G` with `x` having finite additive order, `y` is in the additive submonoid generated by `x` if and only if `y` is in the additive subgroup generated by `x`.
|
AddMonoidHom.isOfFinAddOrder
theorem AddMonoidHom.isOfFinAddOrder :
∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] (f : G →+ H) {x : G},
IsOfFinAddOrder x → IsOfFinAddOrder (f x)
This theorem states that for any given additive monoids `G` and `H`, and for any homomorphism `f` from `G` to `H`, if an element `x` of `G` has finite additive order, then the image of `x` under `f` also has finite additive order. In other words, if there exists a positive integer `n` such that `n * x = 0` in `G`, then there also exists a positive integer (possibly different) `n` such that `n * f(x) = 0` in `H`. This captures the idea that homomorphisms preserve the property of having finite additive order.
More concisely: If `f` is a homomorphism between additive monoids `G` and `H`, and `x` in `G` has finite additive order `n`, then `f(x)` has finite additive order `n` in `H`.
|
IsOfFinOrder.orderOf_pos
theorem IsOfFinOrder.orderOf_pos : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x → 0 < orderOf x := by
sorry
The theorem `IsOfFinOrder.orderOf_pos` states that for any monoid `G` and an element `x` of that monoid, if `x` is of finite order, then the order of `x` is a positive integer. In other words, if there exists a non-zero natural number `n` such that `x^n = 1` in the monoid `G`, then the smallest such `n` (the order of `x`) is greater than zero.
More concisely: In a monoid, if an element has finite order then its order is a positive integer.
|
pow_card_eq_one'
theorem pow_card_eq_one' : ∀ {G : Type u_6} [inst : Group G] {x : G}, x ^ Nat.card G = 1
The theorem `pow_card_eq_one'` states that for any type `G` which has a group structure (denoted by `[inst : Group G]`), for any element `x` of `G`, raising `x` to the power of the cardinality of `G` equals the identity element `1` in the group. This suggests that any group element to the power of the group's cardinality gives the identity of the group. If `G` is infinite, `Nat.card G = 0` and any element to the power of zero gives the identity in the group context.
More concisely: For any group `G` and any of its elements `x`, the power `x^(card G)` equals the identity `1_G` if `G` is finite, and equals `1_G` for the identity element and `1` for any other element if `G` is infinite.
|
zpow_mod_orderOf
theorem zpow_mod_orderOf : ∀ {G : Type u_1} [inst : Group G] (x : G) (z : ℤ), x ^ (z % ↑(orderOf x)) = x ^ z
The theorem `zpow_mod_orderOf` states that for any group `G` and any element `x` of `G`, and for any integer `z`, the power of `x` raised to the value of `z` modulo the order of `x` is equal to the power of `x` raised to `z`. This theorem essentially encapsulates the property of periodicity in the powers of an element in a group, reflecting that once we cycle through the order of the element, we return to the beginning of the cycle.
More concisely: For any group `G`, element `x` of `G`, and integer `z`, `x^(z mod order of x) = x^z` holds.
|
addOrderOf_pos_iff
theorem addOrderOf_pos_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, 0 < addOrderOf x ↔ IsOfFinAddOrder x := by
sorry
The theorem `addOrderOf_pos_iff` states that for any element `x` of an additive monoid `G`, `x` has finite additive order if and only if its order is positive. More specifically, there exists a natural number `n` greater than `0` such that `n • x = 0` (indicating finite additive order) if and only if `x` possesses a positive additive order, as captured by the function `addOrderOf x > 0`.
More concisely: A element `x` in an additive monoid has finite additive order if and only if its positive additive order exists.
|
orderOf_dvd_card
theorem orderOf_dvd_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, orderOf x ∣ Fintype.card G
The theorem `orderOf_dvd_card` states that for any finite group `G` and any element `x` of `G`, the order of `x` divides the cardinality of the group `G`. In other words, if we denote the order of `x` (the smallest natural number `n` such that `x^n = 1` in the group `G` or `0` if there's no such number) as `orderOf x`, and the number of elements in `G` as `Fintype.card G`, then `orderOf x` is a divisor of `Fintype.card G`. This result is a fundamental fact in group theory, often referred to as Lagrange's theorem.
More concisely: The order of any element in a finite group divides the group's cardinality.
|
Commute.isOfFinOrder_mul
theorem Commute.isOfFinOrder_mul :
∀ {G : Type u_1} [inst : Monoid G] {x y : G},
Commute x y → IsOfFinOrder x → IsOfFinOrder y → IsOfFinOrder (x * y)
This theorem states that in any monoid `G`, if `x` and `y` are two elements that commute (i.e., `x * y = y * x`), and both `x` and `y` are of finite order (meaning there exists some `n ≥ 1` such that `x^n = 1` and `y^m = 1`), then their product `x * y` is also of finite order. In other words, two commuting elements of finite order in a monoid are closed under multiplication.
More concisely: In a monoid, if two commuting elements of finite order exist, then their product also has finite order.
|
Subgroup.orderOf_coe
theorem Subgroup.orderOf_coe : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (a : ↥H), orderOf ↑a = orderOf a := by
sorry
This theorem, `Subgroup.orderOf_coe`, states that for any group `G` and any subgroup `H` of `G`, the order of an element `a` in `H` (when viewed as an element of `G`, i.e., `↑a`) is the same as the order of `a` in `H`. In other words, it confirms that the order of an element doesn't change even if we consider it as part of a larger group. The order of an element `x` in a monoid is the smallest positive integer `n` such that `x^n = 1`, or `0` if such an `n` doesn't exist (i.e., `x` is of infinite order).
More concisely: For any group `G` and subgroup `H` of `G`, the order of any element `a` in `H` is equal to its order in `G`.
|
orderOf_eq_zero_iff
theorem orderOf_eq_zero_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x = 0 ↔ ¬IsOfFinOrder x
The theorem `orderOf_eq_zero_iff` states that for any type `G` that forms a monoid, and any element `x` of that monoid, the order of `x` is zero if and only if `x` is not of finite order. In other words, if `x` is an element of a monoid that does not satisfy the property of having a finite order (i.e., there does not exist a positive integer `n` such that `x^n=1`), then by definition, the order of `x` is zero. Conversely, if the order of `x` is zero, it means that `x` does not have a finite order.
More concisely: For any monoid element x, its order is zero if and only if x is of infinite order.
|
isPeriodicPt_mul_iff_pow_eq_one
theorem isPeriodicPt_mul_iff_pow_eq_one :
∀ {G : Type u_1} [inst : Monoid G] {n : ℕ} (x : G), Function.IsPeriodicPt (fun x_1 => x * x_1) n 1 ↔ x ^ n = 1 := by
sorry
The theorem `isPeriodicPt_mul_iff_pow_eq_one` states that for any type `G` that is a monoid, a point `x` in `G` is a periodic point of the function `f(x_1) = x * x_1` of period `n` if and only if `x` raised to the power `n` is equal to the identity element `1` in `G`. A periodic point here means that applying the function `n` times to `1` results in `1` again, essentially indicating that the function cyclically returns to `1` after `n` applications.
More concisely: A point in a monoid is periodic of period n for the function x ↦ x * x\_1 if and only if x^n = 1.
|
addOrderOf_pos
theorem addOrderOf_pos :
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [inst_1 : Finite G] (x : G), 0 < addOrderOf x
The theorem `addOrderOf_pos` states that for any type `G`, which is an instance of a finite, left-cancellable additive monoid, and for any element `x` of `G`, the additive order of `x` is positive. In other words, there is a positive natural number `n` such that `n` additively applied to `x` equals zero, and this number is least among all such natural numbers. This theorem is essentially a variant of `IsOfFinAddOrder.addOrderOf_pos`, but with one fewer assumption since the finiteness of the monoid is automatically guaranteed in this context.
More concisely: For any finite, left-cancellable additive monoid G and its element x, there exists a positive natural number n such that x + ... + x (n times) = 0, and this number n is minimal.
|
orderOf_pos
theorem orderOf_pos : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G] (x : G), 0 < orderOf x := by
sorry
This theorem states that for any object `x` of a given type `G`, under the conditions that `G` is a Left Cancellative Monoid and finite, the order of `x` is always positive. In other words, there exists a positive integer `n` such that `x ^ n = 1`. The theorem does not require an explicit assumption for this since a Left Cancellative Monoid is inherently finite.
More concisely: In a finite Left Cancellative Monoid, every non-identity element has a finite order.
|
isOfFinOrder_iff_pow_eq_one
theorem isOfFinOrder_iff_pow_eq_one :
∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1
The theorem `isOfFinOrder_iff_pow_eq_one` states that for any type `G` that forms a monoid, and any element `x` of `G`, `x` is of finite order (as defined by `IsOfFinOrder`) if and only if there exists a positive integer `n` such that `x` raised to the power of `n` equals the identity element of the monoid. In other words, an element `x` in a monoid is of finite order if it eventually reaches the monoid's identity when repeatedly multiplied by itself for a finite number of times.
More concisely: An element in a monoid is of finite order if and only if there exists a positive integer n such that x ^ n = id, where x is an element of the monoid, id is the identity element, and ^ represents monoid multiplication.
|
Nat.card_submonoidPowers
theorem Nat.card_submonoidPowers :
∀ {G : Type u_1} [inst : LeftCancelMonoid G] {a : G}, Nat.card ↥(Submonoid.powers a) = orderOf a
The theorem `Nat.card_submonoidPowers` asserts that for any left cancellative monoid `G` and any element `a` of `G`, the cardinality of the submonoid generated by `a` (as a natural number) is equal to the order of `a`. In other words, the number of distinct powers of `a` is equal to the smallest positive natural number `n` such that `a^n = 1`, if such `n` exists. If `a` is of infinite order, both are zero by convention.
More concisely: For any left cancellative monoid `G` and its element `a`, the number of distinct powers of `a` equals the order of `a`, or both are zero if `a` has infinite order.
|
addOrderOf_dvd_of_nsmul_eq_zero
theorem addOrderOf_dvd_of_nsmul_eq_zero :
∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n • x = 0 → addOrderOf x ∣ n
The theorem `addOrderOf_dvd_of_nsmul_eq_zero` states that for any type `G` that is an additive monoid, for any element `x` of `G`, and for any natural number `n`, if `n` times `x` equals zero, then the additive order of `x` divides `n`. In other words, if the multiple of an element `x` with natural number `n` makes the total sum zero, then `n` must be a multiple of the additive order of `x`.
More concisely: If `x` is an element of an additive monoid `G` and `n` is a natural number such that `n * x = 0` in `G`, then the additive order of `x` divides `n`.
|
orderOf_dvd_iff_pow_eq_one
theorem orderOf_dvd_iff_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, orderOf x ∣ n ↔ x ^ n = 1 := by
sorry
The theorem `orderOf_dvd_iff_pow_eq_one` states that for any type `G` equipped with the structure of a monoid and for any element `x` of `G` and natural number `n`, the order of element `x` divides `n` if and only if `x` raised to the power `n` equals the multiplicative identity element `1`. In other words, the exponent at which `x` gives `1` is a divisor of `n` if and only if the `n`-th power of `x` is `1`.
More concisely: For any monoid `G` and `x` in `G` and natural number `n`, `x` raised to the power `n` equals the identity element `1` if and only if the order of `x` divides `n`.
|
mod_addOrderOf_zsmul
theorem mod_addOrderOf_zsmul :
∀ {G : Type u_1} [inst : AddGroup G] (x : G) (z : ℤ), (z % ↑(addOrderOf x)) • x = z • x
The theorem `mod_addOrderOf_zsmul` states that for any additive group `G` and any element `x` of `G`, and for any integer `z`, the action of multiplying `x` by `z` modulo the additive order of `x` is the same as simply multiplying `x` by `z`. In mathematical terms, for any `z ∈ ℤ`, we have `(z mod addOrderOf(x)) • x = z • x`. This means that the cyclic behavior of `x` under addition is captured completely by its additive order, and any excess multiplication "wraps around" just like clock arithmetic.
More concisely: For any additive group G, element x of G, and integer z, (z mod additiveOrderOf x) * x = z * x.
|
orderOf_pos_iff
theorem orderOf_pos_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, 0 < orderOf x ↔ IsOfFinOrder x
This theorem states that for any group element `x` in a monoid `G`, the element `x` has finite order if and only if its order is positive. In other words, there exists a positive integer `n` such that `x ^ n = 1` (which means `x` has finite order or `x` is of finite order) if and only if the order of `x` is greater than zero. This provides a condition for determining whether a group element has finite order in terms of its order being positive.
More concisely: A group element x in a monoid has finite order if and only if its order is a positive integer.
|
pow_mod_orderOf
theorem pow_mod_orderOf : ∀ {G : Type u_1} [inst : Monoid G] (x : G) (n : ℕ), x ^ (n % orderOf x) = x ^ n
The theorem `pow_mod_orderOf` states that for any type `G` that has a monoid structure and for any element `x` of `G` and any natural number `n`, the result of raising `x` to the power of `n` modulo the order of `x` is equal to the result of `x` raised to the power of `n`. In mathematical terms, for a given element `x` in a monoid `G` and a natural number `n`, we have \(x^{(n \bmod \text{orderOf}(x))} = x^n\). This implies that the power operation on `x` is periodic with period equal to the order of `x`.
More concisely: For any element `x` in a monoid `G` with order `n`, raising `x` to the power of `n` modulo the order of `x` equals raising `x` to the power of any integer `k` congruent to `n` modulo the order of `x`.
|
AddMonoid.addOrderOf_eq_one_iff
theorem AddMonoid.addOrderOf_eq_one_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x = 1 ↔ x = 0 := by
sorry
The theorem `AddMonoid.addOrderOf_eq_one_iff` states that for any type `G` that has an additive monoid structure, given an element `x` of `G`, the "additive order" of `x` is equal to 1 if and only if `x` is the additive identity (0) of the monoid. In other words, in any additive monoid, an element has order 1 (the minimal number of times the element needs to be added to itself to reach the identity) if and only if it is the identity element.
More concisely: For any additive monoid G and its element x, x has additive order 1 if and only if x is the additive identity of G.
|
MonoidHom.isOfFinOrder
theorem MonoidHom.isOfFinOrder :
∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] (f : G →* H) {x : G},
IsOfFinOrder x → IsOfFinOrder (f x)
The theorem `MonoidHom.isOfFinOrder` states that for any two types `G` and `H` with monoid structures and a monoid homomorphism `f` from `G` to `H`, if an element `x` in `G` has finite order (i.e., there exists a natural number `n` greater than or equal to 1 such that `x` to the power of `n` equals the identity element), then the image of `x` under the function `f` also has finite order in `H`. This theorem is a formalization of the property in group theory that the order of an element is preserved under a group homomorphism.
More concisely: If `f` is a monoid homomorphism from monoid `G` to monoid `H` and `x` in `G` has finite order `n`, then `f(x)` has finite order in `H` of at most `n`.
|
orderOf_one
theorem orderOf_one : ∀ {G : Type u_1} [inst : Monoid G], orderOf 1 = 1
The theorem `orderOf_one` states that for any type `G` that forms a Monoid (an algebraic structure with a single associative binary operation and an identity element), the order of the identity element, denoted as `1` in this case, is `1`. In other words, if you raise the identity element to the power of `1`, you get the identity element back, as per the definition of a monoid, and no smaller positive integer will satisfy this condition. Hence, the order of the identity is `1`.
More concisely: For any monoid `G`, the order of its identity element is 1.
|