Monoid.exponent_ne_zero
theorem Monoid.exponent_ne_zero : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G ≠ 0 ↔ Monoid.ExponentExists G
The theorem `Monoid.exponent_ne_zero` states that for any type `G` that is a `Monoid`, the exponent of the monoid is not zero if and only if there exists a positive integer `n` such that every element of the monoid raised to the power `n` equals the identity element. In other words, a monoid has a non-zero exponent exactly when it satisfies the property that all its elements have a common positive integer exponent that yields the identity element when applied.
More concisely: A monoid `G` has a non-zero exponent if and only if there exists a positive integer `n` such that for all `x` in `G`, `x^n = id_G`.
|
AddMonoid.exponent_min'
theorem AddMonoid.exponent_min' :
∀ {G : Type u} [inst : AddMonoid G] (n : ℕ), 0 < n → (∀ (g : G), n • g = 0) → AddMonoid.exponent G ≤ n
The theorem `AddMonoid.exponent_min'` states that for any type `G` which forms an additive monoid, and for any natural number `n` greater than zero, if the scalar multiplication of `n` and any element `g` of `G` equals zero, then the exponent of the additive monoid `G` should be less than or equal to `n`. Here, the exponent of an additive monoid is the smallest positive integer `n` such that `n • g = 0` for all `g` in `G`, or zero if such an integer does not exist.
More concisely: For any additive monoid `G` and natural number `n` greater than zero, if for all `g` in `G`, `n * g = 0`, then the exponent of `G` is less than or equal to `n`.
|
Monoid.pow_exponent_eq_one
theorem Monoid.pow_exponent_eq_one : ∀ {G : Type u} [inst : Monoid G] (g : G), g ^ Monoid.exponent G = 1
This theorem states that for any given group `G` and any element `g` in `G`, raising `g` to the power of the exponent of `G` will always yield the identity element of the group. This exponent is the smallest positive integer such that this property holds for all elements of the group, or it is zero if no such integer exists. The identity element of a group is the element that, when multiplied with any element of the group, leaves the other element unchanged.
More concisely: For any group `G` and its identity element `e`, for all elements `g` in `G`, there exists an integer `n` such that `g^n = e`.
|
inv_eq_self_of_exponent_two
theorem inv_eq_self_of_exponent_two : ∀ {G : Type u} [inst : Group G], Monoid.exponent G = 2 → ∀ (x : G), x⁻¹ = x := by
sorry
This theorem states that in a group whose exponent is two, every element is its own inverse. In other words, for any group 'G' where the smallest positive integer 'n' such that raising any element 'g' of 'G' to the power of 'n' yields the identity (and this 'n' is 2), the inverse of any element 'x' in the group is equal to 'x' itself.
More concisely: In a group of order 2, every element is its own inverse.
|
Monoid.exponent_dvd
theorem Monoid.exponent_dvd :
∀ {G : Type u} [inst : Monoid G] {n : ℕ}, Monoid.exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n
This theorem states that for any group `G` and any natural number `n`, the exponent of the group `G` divides `n` if and only if the order of each element `g` in `G` divides `n`. Here, the exponent of a group is the smallest positive integer `n` such that raising any group element `g` to the power of `n` results in the identity element (`g ^ n = 1`), if such an integer exists, otherwise it's conventionally zero. Similarly, the order of a group element is the smallest positive integer `n` such that raising the given element to the power of `n` results in the identity element (`x ^ n = 1`), or zero if the element is of infinite order.
More concisely: For any group `G` and natural number `n`, the group's exponent `n` equals the lcm (least common multiple) of the orders of all its elements.
|
Monoid.lcm_orderOf_eq_exponent
theorem Monoid.lcm_orderOf_eq_exponent :
∀ {G : Type u} [inst : Monoid G] [inst_1 : Fintype G], Finset.univ.lcm orderOf = Monoid.exponent G
The theorem `Monoid.lcm_orderOf_eq_exponent` states that for any type `G` that has a monoid structure and is also a finite type, the least common multiple (lcm) of the order of each element in the universal finite set (`Finset.univ`) is equal to the exponent of the monoid `G`. In other words, the smallest positive integer `n` such that raising any element of the group to the power of `n` yields the identity element (if such an integer exists), is equal to the least common multiple of the orders of all elements in the group. If no such integer exists, the convention is to return `0`.
More concisely: For any finite monoid `G`, the least common multiple of the orders of its elements equals the exponent of the monoid `G`. If no such common exponent exists, the result is `0`.
|
Monoid.exponent_prod
theorem Monoid.exponent_prod :
∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Monoid M₁] [inst_1 : Monoid M₂],
Monoid.exponent (M₁ × M₂) = lcm (Monoid.exponent M₁) (Monoid.exponent M₂)
This theorem states that the exponent of the product of two monoids is the least common multiple (lcm) of the exponents of the individual monoids. Here, the exponent of a monoid is defined as the smallest positive integer `n` such that raising any element of the monoid to the power `n` results in the identity element of the monoid, if such an integer exists, otherwise it is zero. In mathematical notation, if `M₁` and `M₂` are two monoids, then the exponent of the product monoid `M₁ × M₂` is equal to the lcm of the exponents of `M₁` and `M₂`.
More concisely: The exponent of the product of two monoids is the least common multiple of their exponents.
|
Monoid.exponent_pos_of_exists
theorem Monoid.exponent_pos_of_exists :
∀ {G : Type u} [inst : Monoid G] (n : ℕ), 0 < n → (∀ (g : G), g ^ n = 1) → 0 < Monoid.exponent G
The theorem 'Monoid.exponent_pos_of_exists' asserts that for any type 'G' equipped with a monoid structure, given a positive integer 'n' such that every element 'g' of 'G' raised to the power 'n' equals the identity element (i.e., 'g ^ n = 1'), the exponent of the monoid 'G' is always positive. In simpler terms, if there exists a positive integer power that makes all elements of a monoid equal to the identity element, then the smallest such power (which is the exponent of the monoid) must be a positive number.
More concisely: For any monoid G and positive integer n such that g^n = 1 for all g in G, the exponent of G is positive.
|
MonoidHom.exponent_dvd
theorem MonoidHom.exponent_dvd :
∀ {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : Monoid M₁] [inst_1 : Monoid M₂] [inst_2 : FunLike F M₁ M₂]
[inst_3 : MonoidHomClass F M₁ M₂] {f : F}, Function.Surjective ⇑f → Monoid.exponent M₂ ∣ Monoid.exponent M₁
The theorem `MonoidHom.exponent_dvd` states that for any surjective homomorphism `f` from a monoid `M₁` to another monoid `M₂`, the exponent of `M₂` divides the exponent of `M₁`. Here, a function is considered surjective if for every element in the codomain, there is at least one element in the domain that maps to it under the function. The exponent of a monoid is defined as the smallest positive integer `n` such that raising any element of the monoid to the `n`th power results in the identity element; if no such `n` exists, the exponent is defined to be zero. A monoid homomorphism is a function between two monoids that preserves the monoid operation and identity.
More concisely: If `f` is a surjective homomorphism from the monoid `M₁` to the monoid `M₂`, then the exponent of `M₂` divides the exponent of `M₁`.
|
AddMonoid.exponent_eq_of_addEquiv
theorem AddMonoid.exponent_eq_of_addEquiv :
∀ {G : Type u} [inst : AddMonoid G] {H : Type u_1} [inst_1 : AddMonoid H],
G ≃+ H → AddMonoid.exponent G = AddMonoid.exponent H
The theorem states that if there exists an additive equivalence (a bijective function that preserves addition) between two types `G` and `H`, both equipped with an additive monoid structure, then the exponent of `G` is equal to the exponent of `H`. Remember, the exponent of an additive group `G` is the smallest positive integer `n` such that `n • g = 0` for all `g` in `G`, if such an integer exists; otherwise, it is zero by convention. So this theorem is saying that if there's a structure-preserving bijection between two additive groups, their exponents are also the same.
More concisely: If two additive groups, equipped with bijective additive equivalences between them, have identical additive identities and associative binary operations, then they have equal exponents.
|
AddMonoid.exponent_nsmul_eq_zero
theorem AddMonoid.exponent_nsmul_eq_zero : ∀ {G : Type u} [inst : AddMonoid G] (g : G), AddMonoid.exponent G • g = 0
The theorem `AddMonoid.exponent_nsmul_eq_zero` states that for any given additive monoid `G` and any element `g` of `G`, if you add `g` to itself `AddMonoid.exponent G` times, the result will be the zero element of `G`. In other words, the `AddMonoid.exponent G` is the smallest positive integer such that `n • g = 0` for all `g` in `G` if it exists, otherwise it is zero by convention.
More concisely: For any additive monoid G and element g in G, the power g^(AddMonoid.exponent G) equals the additive identity in G.
|
Monoid.exponent_eq_of_mulEquiv
theorem Monoid.exponent_eq_of_mulEquiv :
∀ {G : Type u} [inst : Monoid G] {H : Type u_1} [inst_1 : Monoid H],
G ≃* H → Monoid.exponent G = Monoid.exponent H
The theorem `Monoid.exponent_eq_of_mulEquiv` states that for any two groups `G` and `H`, if there exists a multiplication-preserving equivalence (an isomorphism) between `G` and `H`, then the exponent of `G` is equal to the exponent of `H`. Here, the exponent of a group is defined as the smallest positive integer `n` such that every element of the group raised to the power `n` equals the identity, if such an integer exists; otherwise, it is conventionally defined as zero.
More concisely: If there exists an isomorphism between groups `G` and `H` that preserves group multiplication, then the exponent of `G` equals the exponent of `H`.
|
AddMonoid.exponent_pos_of_exists
theorem AddMonoid.exponent_pos_of_exists :
∀ {G : Type u} [inst : AddMonoid G] (n : ℕ), 0 < n → (∀ (g : G), n • g = 0) → 0 < AddMonoid.exponent G
This theorem states that for any type `G`, which is an instance of an additive monoid, and any positive natural number `n`, if `n` is such that the `n`-fold sum of any element `g` of `G` equals the additive identity (0), then the exponent of the additive monoid `G` is positive. The exponent of an additive monoid is the smallest positive natural number that makes the `n`-fold sum of each element equal to 0, or else it is defined to be 0 by convention if no such number exists.
More concisely: If a type `G` is an additive monoid and every element `g` in `G` satisfies the property that the sum of `g` with itself `n` times equals the additive identity `0`, then the exponent of `G` is positive.
|
Monoid.exponent_eq_prime_iff
theorem Monoid.exponent_eq_prime_iff :
∀ {G : Type u_1} [inst : Monoid G] [inst_1 : Nontrivial G] {p : ℕ},
p.Prime → (Monoid.exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p)
This theorem states that for any nontrivial monoid `G` and a prime number `p`, `p` is the exponent of the monoid if and only if the order of every non-identity element of `G` equals `p`. Here, a nontrivial monoid means a monoid that has at least two distinct elements. The exponent of a monoid is the smallest positive integer `n` such that every element of the monoid raised to the power `n` equals the identity, if such an integer exists; otherwise, it's zero. The order of an element of a monoid is the smallest positive integer `m` such that the element raised to the power `m` equals the identity, if such an integer exists; otherwise, it's zero. A prime number in this context is a number that is not zero, not a unit, and has the property that if it divides the product of two numbers, then it must divide at least one of them.
More concisely: For a nontrivial monoid G and a prime number p, p is the exponent of G if and only if the order of every non-identity element of G equals p.
|
AddMonoid.lcm_addOrderOf_eq_exponent
theorem AddMonoid.lcm_addOrderOf_eq_exponent :
∀ {G : Type u} [inst : AddMonoid G] [inst_1 : Fintype G], Finset.univ.lcm addOrderOf = AddMonoid.exponent G := by
sorry
This theorem states that for any type `G` that is an instance of an `AddMonoid` and `Fintype`, the least common multiple (lcm) of the orders of all elements in the universal finite set (`Finset.univ`) equals to the exponent of the additive monoid. In other words, the least common multiple of the numbers obtained by applying the function `addOrderOf` to each element of the universal finite set is equal to the exponent of the additive monoid `G`. The `addOrderOf` function represents the order of an element in the group, while the `exponent` of an additive group is defined as the smallest positive integer `n` such that `n • g = 0` for all `g ∈ G`, if it exists.
More concisely: For any additive monoid and finite type `G` in Lean 4, the least common multiple of the orders of all elements in `Finset.univ` equals the exponent of the additive monoid `G`.
|
AddMonoid.exponent_pi
theorem AddMonoid.exponent_pi :
∀ {ι : Type u_1} [inst : Fintype ι] {M : ι → Type u_2} [inst_1 : (i : ι) → AddMonoid (M i)],
AddMonoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => AddMonoid.exponent (M x)
The theorem `AddMonoid.exponent_pi` states that for any finite type `ι` and a function `M` that takes an element of `ι` and outputs a type, given that each output type of `M` is an additive monoid, the exponent of the cartesian product of these additive monoids (which is itself an additive monoid) is equal to the least common multiple (lcm) of the exponents of the individual additive monoids, where the lcm is computed over the entire universal set of `ι`. In mathematical terms, if `M i` are additive monoids for each `i` in a finite set, the exponent of the product monoid is the least common multiple of the exponents of `M i`.
More concisely: For any finite type `ι` and functions `M : ι → Type` such that each `M i` is an additive monoid, the exponent of the product monoid of `M i`'s is equal to the least common multiple of their exponents.
|
AddMonoid.exponent_eq_zero_iff
theorem AddMonoid.exponent_eq_zero_iff :
∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = 0 ↔ ¬AddMonoid.ExponentExists G
This theorem states that for any additive monoid `G`, the exponent of `G` equals to `0` if and only if there does not exist a positive integer `n` such that `n • g = 0` for all `g` in `G`. In other words, the exponent of an additive monoid is zero if and only if it's impossible to find a positive integer that when scaled by any element of the group results in the additive identity (zero).
More concisely: The additive monoid has exponent 0 if and only if there is no positive integer that annihilates all its elements.
|
mul_comm_of_exponent_two
theorem mul_comm_of_exponent_two :
∀ {G : Type u} [inst : Monoid G] [inst_1 : IsCancelMul G], Monoid.exponent G = 2 → ∀ (a b : G), a * b = b * a := by
sorry
The theorem `mul_comm_of_exponent_two` states that for any type `G` that has a monoid structure and a cancel multiplication property (a cancellative monoid), if the exponent of the monoid is two, then all elements of the monoid commute. In other words, for any two elements `a` and `b` in the monoid, the multiplication of `a` and `b` equals the multiplication of `b` and `a`. In mathematical terms, if a cancellative monoid has an exponent of 2 (meaning every element squared equals the identity), then for any `a` and `b` in the monoid, `a * b = b * a`.
More concisely: In a cancellative monoid with exponent two, all elements commute with each other, i.e., for all a and b in the monoid, a * b = b * a.
|
AddMonoid.exponent_prod
theorem AddMonoid.exponent_prod :
∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : AddMonoid M₁] [inst_1 : AddMonoid M₂],
AddMonoid.exponent (M₁ × M₂) = lcm (AddMonoid.exponent M₁) (AddMonoid.exponent M₂)
The theorem states that the exponent of the product of two additive monoids is the least common multiple (LCM) of the exponents of the individual additive monoids. Here, an additive monoid is a type with an addition operation satisfying certain properties, and its exponent is the smallest positive integer n such that n times any element in the monoid gives the additive identity, if such an n exists, or zero otherwise. The product of two additive monoids is the set of pairs of elements from each monoid, with addition defined component-wise, and its exponent is defined similarly. The theorem asserts that the exponent of this product monoid is the LCM of the exponents of the original monoids.
More concisely: The exponent of the product of two additive monoids is the least common multiple of their exponents.
|
Monoid.exponent_pi
theorem Monoid.exponent_pi :
∀ {ι : Type u_1} [inst : Fintype ι] {M : ι → Type u_2} [inst_1 : (i : ι) → Monoid (M i)],
Monoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => Monoid.exponent (M x)
The theorem `Monoid.exponent_pi` states that for any type `ι` (with a finite number of elements) and a function `M` mapping each element of `ι` to a Monoid, the exponent of the product of all these Monoids (where the product is taken over all elements of `ι`) is equal to the least common multiple (LCM) of the exponents of each individual Monoid. Here, the exponent of a Monoid is defined as the smallest positive integer `n` such that raising any element of the Monoid to the power `n` gives the identity element (or zero if no such `n` exists), and `Finset.univ` represents the set of all elements of `ι`.
More concisely: For any finite type `ι` and a function `M : ∀ i, Monoid (M i)`, the exponent of the product of `M i` for all `i` in `ι` equals the least common multiple of the exponents of each `M i`.
|
inv_eq_self_of_orderOf_eq_two
theorem inv_eq_self_of_orderOf_eq_two : ∀ {G : Type u} [inst : Group G] {x : G}, orderOf x = 2 → x⁻¹ = x
The theorem `inv_eq_self_of_orderOf_eq_two` states that for any element `x` in a group `G`, if `x` has order two (i.e., `x` squared equals the identity element), then `x` is its own inverse. In other words, the inverse of `x` is `x` itself. This theorem applies to any group `G`, and it is a statement about the structure of the group and its elements.
More concisely: If an element `x` in a group `G` has order two, then `x` is its own inverse (i.e., `x * x = id_G` implies `x * x = x * inverse x`).
|
AddMonoid.exponent_dvd
theorem AddMonoid.exponent_dvd :
∀ {G : Type u} [inst : AddMonoid G] {n : ℕ}, AddMonoid.exponent G ∣ n ↔ ∀ (g : G), addOrderOf g ∣ n
The theorem `AddMonoid.exponent_dvd` states that for every type `G` which is an additive monoid, and for every natural number `n`, the exponent of the additive monoid `G` divides `n` if and only if the order of each element `g` in the group `G` divides `n`. Here, the order of an element `g` refers to the smallest positive integer `n` such that `n` times `g` equals zero, if such an `n` exists. If `n` doesn't exist (i.e., `g` is of infinite order), the order of `g` is conventionally defined as zero. The exponent of an additive group `G` is the smallest positive integer `n` such that `n` times `g` equals zero for all `g` in `G`, if such an `n` exists; otherwise, the exponent is conventionally defined as zero.
More concisely: For every additive monoid G and natural number n, the exponent of G divides n if and only if the order of every element in G divides n.
|
Monoid.exponent_dvd_of_forall_pow_eq_one
theorem Monoid.exponent_dvd_of_forall_pow_eq_one :
∀ {G : Type u} [inst : Monoid G] {n : ℕ}, (∀ (g : G), g ^ n = 1) → Monoid.exponent G ∣ n
This theorem states that for any type `G` that is a Monoid, and any natural number `n`, if for every element `g` in `G`, `g` raised to the power `n` is equal to the identity element `1`, then the exponent of Monoid `G` divides `n`. In mathematical terms, this is stating that if ∀g ∈ G, g^n = 1, then the exponent of the group G divides n.
More concisely: If every element in a monoid `G` raises any natural number `n` to the power equal to the identity element `1`, then the exponent of `G` divides `n`.
|
Monoid.order_dvd_exponent
theorem Monoid.order_dvd_exponent : ∀ {G : Type u} [inst : Monoid G] (g : G), orderOf g ∣ Monoid.exponent G
The theorem `Monoid.order_dvd_exponent` asserts that for any type `G` and its instance of a `Monoid`, for any element `g` of `G`, the order of `g` divides the exponent of the `Monoid`. In other words, if `n` is the smallest positive integer such that `g^n = 1` (the order of `g`) and `m` is the smallest positive integer such that for all `x` in `G`, `x^m = 1` (the exponent of the Monoid), then `n` divides `m`. This means that `m` is a multiple of `n` in the set of natural numbers.
More concisely: For any Monoid `G` and its identity element `e`, the order of any element `g` in `G` divides the exponent of `G`, i.e., the order of `g` is a divisor of the order of the identity element.
|
AddMonoid.addOrder_dvd_exponent
theorem AddMonoid.addOrder_dvd_exponent :
∀ {G : Type u} [inst : AddMonoid G] (g : G), addOrderOf g ∣ AddMonoid.exponent G
The theorem `AddMonoid.addOrder_dvd_exponent` states that for any additive monoid `G` and an element `g` in `G`, the additive order of `g` (denoted by `addOrderOf g`) divides the exponent of the additive monoid `G` (denoted by `AddMonoid.exponent G`). In other words, the order of any element in the monoid is a divisor of the monoid's exponent. This is the sense in which the order of an element can be seen as a measure of the "cyclicity" of that element, and the exponent as a measure of the overall "cyclicity" of the monoid.
More concisely: For any additive monoid G and its element g, the additive order of g divides the exponent of G.
|
AddMonoid.exponent_ne_zero
theorem AddMonoid.exponent_ne_zero :
∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G ≠ 0 ↔ AddMonoid.ExponentExists G
The theorem `AddMonoid.exponent_ne_zero` states that for any type `G` that has an additive monoid structure, the exponent of the additive monoid `G` is not zero if and only if there exists a positive integer `n` such that `n • g = 0` for all `g` in `G`. Here, `n • g` denotes the n-fold addition of `g` with itself. In other words, the exponent of an additive monoid is nonzero if and only if the condition of the `ExponentExists` predicate is satisfied.
More concisely: The exponent of an additive monoid is nonzero if and only if there exists a positive integer that annihilates every element in the monoid under n-fold addition.
|
Monoid.exponent_min'
theorem Monoid.exponent_min' :
∀ {G : Type u} [inst : Monoid G] (n : ℕ), 0 < n → (∀ (g : G), g ^ n = 1) → Monoid.exponent G ≤ n
The theorem `Monoid.exponent_min'` states that for any monoid `G` and any positive natural number `n`, if every element `g` of the monoid `G` satisfies the property that `g` raised to power `n` equals the identity element (`g ^ n = 1`), then the exponent of the monoid `G` is less than or equal to `n`. This is essentially saying that the exponent of a monoid, defined as the smallest positive integer `n` such that `g ^ n = 1` for all `g` in `G` (or zero if such an `n` doesn't exist), must be the smallest such `n` that satisfies this property for all `g` in `G`.
More concisely: If every element in a monoid raises any positive power to the power of its exponent equal to the identity element, then the monoid's exponent is less than or equal to that power.
|
Monoid.exponent_eq_zero_iff
theorem Monoid.exponent_eq_zero_iff :
∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = 0 ↔ ¬Monoid.ExponentExists G
The theorem `Monoid.exponent_eq_zero_iff` states that for any given monoid `G`, the exponent of `G` is zero if and only if there does not exist a positive integer `n` such that raising any element of `G` to the power `n` results in the identity element. In terms of the monoid, this means there is no common positive exponent to which every element in the monoid can be raised to yield the identity.
More concisely: A monoid has exponent 0 if and only if there is no positive integer n such that every element raised to the power n equals the identity.
|
AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero
theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero :
∀ {G : Type u} [inst : AddMonoid G] {n : ℕ}, (∀ (g : G), n • g = 0) → AddMonoid.exponent G ∣ n
The theorem `AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero` states that for any type `G` that has an `AddMonoid` instance, along with any natural number `n`, if for every element `g` of `G` the `n`-fold addition of `g` (denoted as `n • g`) results in the additive identity (0), then the exponent of the additive monoid `G` divides `n`. In simpler terms, if adding any element of the group to itself `n` times results in zero, then the smallest positive number with this property (the exponent of the group) is a divisor of `n`.
More concisely: If for every element in an additive monoid `G`, the `n`-fold addition of that element equals the additive identity, then the exponent of `G` divides `n`.
|