AddCommGroup.add_torsion_eq_add_torsion_submonoid
theorem AddCommGroup.add_torsion_eq_add_torsion_submonoid :
∀ (G : Type u_1) [inst : AddCommGroup G], AddCommMonoid.addTorsion G = (AddCommGroup.torsion G).toAddSubmonoid := by
sorry
This theorem states that, for any abelian group `G`, the additive torsion submonoid of `G` is identical to the torsion subgroup of `G` when the latter is considered as a submonoid. In other words, these two structures, which may appear different, actually contain the same elements when we consider `G` as an additive commutative monoid. The torsion elements are those elements of `G` that have a finite additive order, meaning there is a finite natural number `n` such that adding the element to itself `n` times results in the additive identity (usually zero).
More concisely: The additive torsion submonoid of an abelian group equals the torsion subgroup considered as a submonoid, consisting of elements with finite additive order.
|
IsTorsion.not_torsion_free
theorem IsTorsion.not_torsion_free :
∀ {G : Type u_1} [inst : Group G] [hN : Nontrivial G], Monoid.IsTorsion G → ¬Monoid.IsTorsionFree G
This theorem states that a nontrivial torsion group is not torsion-free. In other words, in the context of a group structure `G` (which is assumed to be nontrivial, meaning it has at least one element that is not the identity), if `G` satisfies the property that all of its elements have finite order (meaning for each element, there is a positive integer `n` such that raising the element to the `n`-th power gives the identity), then it cannot also satisfy the property of being torsion-free (meaning, apart from the identity, none of its elements have finite order).
More concisely: A nontrivial group with every element having finite order is not torsion-free.
|
AddIsTorsion.extension_closed
theorem AddIsTorsion.extension_closed :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
N = f.ker → AddMonoid.IsTorsion H → AddMonoid.IsTorsion ↥N → AddMonoid.IsTorsion G
This theorem asserts that additive torsion groups are closed under extensions. Specifically, for any two types `G` and `H` with `AddGroup` structures, an additive subgroup `N` of `G`, and an additive group homomorphism `f` from `G` to `H`, if `N` is equal to the kernel of `f`, and if both `H` and `N` are torsion groups (i.e., all their elements are of finite order), then `G` is also a torsion group. In other words, if a group and a subgroup are both torsion, then so is any group extension of the subgroup by the group.
More concisely: If `G` is an additive group with `AddGroup` structure, `N` is an additive subgroup of `G` that is also a torsion group, and `f` is an additive group homomorphism from `G` to another additive group `H` with kernel `N`, such that `H` is also a torsion group, then `G` is a torsion group.
|
IsTorsion.exponentExists
theorem IsTorsion.exponentExists :
∀ {G : Type u_1} [inst : Group G],
Monoid.IsTorsion G → (Set.range fun g => orderOf g).Finite → Monoid.ExponentExists G
The theorem states that for any group `G`, if the group `G` is a torsion group, meaning all its elements have finite order, and if the set of all possible orders of elements in `G` is also finite, then there exists a positive integer `n` such that `g^n = 1` for all elements `g` in `G`. In other words, the group exponent exists for any bounded torsion group.
More concisely: In a finitely generated torsion group, there exists a positive integer that raises every element to the power of it, yielding the identity element.
|
IsTorsion.of_surjective
theorem IsTorsion.of_surjective :
∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H},
Function.Surjective ⇑f → Monoid.IsTorsion G → Monoid.IsTorsion H
The theorem `IsTorsion.of_surjective` states that for any two types `G` and `H`, where both `G` and `H` are groups, if there is a surjective group homomorphism `f` from `G` to `H` and `G` is a torsion group (i.e., each element of `G` has finite order), then `H` is also a torsion group. In other words, the image of a surjective torsion group homomorphism is also a torsion group.
More concisely: If `f` is a surjective group homomorphism from a torsion group `G` to group `H`, then `H` is a torsion group.
|
IsTorsionFree.addSubgroup
theorem IsTorsionFree.addSubgroup :
∀ {G : Type u_1} [inst : AddGroup G],
AddMonoid.IsTorsionFree G → ∀ (H : AddSubgroup G), AddMonoid.IsTorsionFree ↥H
This theorem states that if a group 'G' is additively torsion-free, then any subgroup 'H' of 'G' is also additively torsion-free. Here, an additive group 'G' is said to be torsion-free if the only element of 'G' whose addition to itself a finite number of times gives the zero element is the zero element itself. In other words, no non-zero element of the group has a finite additive order. The theorem extends this property to all subgroups of a torsion-free group.
More concisely: If 'G' is an additively torsion-free group, then every subgroup of 'G' is also additively torsion-free.
|
AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul
theorem AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul :
∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} [hp : Fact p.Prime] (g : ↥(AddCommMonoid.primaryComponent G p)),
∃ n, addOrderOf g = p ^ n
The theorem states that for any element `g` in the `p`-primary component of an additive commutative monoid `G`, there exists a nonnegative integer `n` such that the additive order of `g` is `p^n`. Here, `p` is a prime number, the additive order of `g` is the smallest positive integer `n` such that `n` times `g` equals the additive identity (usually zero), and the `p`-primary component of `G` is the subset of elements whose additive order is a power of `p`.
More concisely: Every element in the p-primary component of an additive commutative monoid has additive order equal to some power of the prime p.
|
AddCommMonoid.primaryComponent.disjoint
theorem AddCommMonoid.primaryComponent.disjoint :
∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} [hp : Fact p.Prime] {p' : ℕ} [hp' : Fact p'.Prime],
p ≠ p' → Disjoint (AddCommMonoid.primaryComponent G p) (AddCommMonoid.primaryComponent G p')
The theorem states that for any additive commutative monoid `G` and any two distinct prime numbers `p` and `p'`, the `p`-primary and `p'`-primary components of `G` are disjoint. The `p`-primary component of `G` is the set of elements whose additive order is a power of `p`, and similarly for the `p'`-primary component. Two components are considered disjoint if the infimum (greatest lower bound) of any element from each component is the bottom element of the lattice.
More concisely: For any additive commutative monoid G and distinct prime numbers p and p', the p-primary and p'-primary components of G have no elements in common.
|
is_add_torsion_of_finite
theorem is_add_torsion_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Finite G], AddMonoid.IsTorsion G := by
sorry
This theorem states that all finite additive groups are additive torsion groups. That is, for any group `G` of type `u_1` that has the structures of an additive group and is finite, every element in `G` is of finite additive order. In mathematical terms, each element in such a group has some positive integer `n` such that the sum of `n` copies of the element is equal to the additive identity of the group.
More concisely: Every element in a finite additive group has finite additive order.
|
AddMonoid.IsTorsionFree.prod
theorem AddMonoid.IsTorsionFree.prod :
∀ {η : Type u_3} {Gs : η → Type u_4} [inst : (i : η) → AddGroup (Gs i)],
(∀ (i : η), AddMonoid.IsTorsionFree (Gs i)) → AddMonoid.IsTorsionFree ((i : η) → Gs i)
The theorem states that if we take a direct product of additive torsion-free groups, the resulting group is also torsion-free. In other words, given a family of types `Gs` indexed by a type `η`, where each type in the family forms an additive group and is torsion-free (i.e., the only element with finite additive order is the zero element), then the direct product of these types, seen as an additive group, is also torsion-free.
More concisely: If `Gs` is a family of additive torsion-free groups indexed by a type `η`, then their direct product is also a torsion-free additive group.
|
IsAddTorsion.exponentExists
theorem IsAddTorsion.exponentExists :
∀ {G : Type u_1} [inst : AddGroup G],
AddMonoid.IsTorsion G → (Set.range fun g => addOrderOf g).Finite → AddMonoid.ExponentExists G
This theorem states that for any additive torsion group 'G' that is bounded, the group exponent exists. Here, an additive torsion group is defined as a group where every element has a finite additive order, i.e., for all elements 'g' in 'G', there exists a positive integer 'n' such that 'n' times 'g' equals zero. The group being bounded refers to the set of all additive orders of all elements in 'G' being finite. The existence of a group exponent means there is a positive integer 'n' such that 'n' times any element in 'G' equals zero. In other words, if 'G' is a bounded additive torsion group, then there exists a common positive integer 'n' that annihilates all elements of 'G' when scaled with.
More concisely: A bounded additive torsion group has a common finite order.
|
AddMonoid.IsTorsion.not_torsion_free
theorem AddMonoid.IsTorsion.not_torsion_free :
∀ {G : Type u_1} [inst : AddGroup G] [hN : Nontrivial G], AddMonoid.IsTorsion G → ¬AddMonoid.IsTorsionFree G := by
sorry
This theorem states that a nontrivial additive torsion group cannot be torsion-free. More specifically, if we have an additive group `G` with a nontrivial structure (that is, it contains at least one element other than the zero element), and if every element of `G` has finite additive order (meaning that for every element, there is a non-zero integer such that the sum of that many copies of the element equals zero), then it is not the case that `G` is torsion-free (meaning that the only element of `G` with finite order is the zero element). In other words, in an additive group where every element has finite order, there must be an element other than zero that has finite order.
More concisely: In an additive group with a nontrivial structure, if every element has finite order, then the group contains a non-zero element of finite order.
|
AddMonoid.IsTorsion.module_of_torsion
theorem AddMonoid.IsTorsion.module_of_torsion :
∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M],
AddMonoid.IsTorsion R → AddMonoid.IsTorsion M
This theorem states that if a module has a set of scalars which are additively torsion, then the module itself is additively torsion. More specifically, for any type `R` and `M`, with `M` being an additive commutative monoid, `R` being a semiring, and `M` being a module over `R`, if `R` satisfies the property that all of its elements are of finite additive order (i.e., `R` is additively torsion, denoted as `AddMonoid.IsTorsion R`), then `M` also satisfies the property that all of its elements are of finite additive order (i.e., `M` is additively torsion, denoted as `AddMonoid.IsTorsion M`).
More concisely: If `R` is an additively torsion semiring and `M` is a module over `R`, then `M` is also an additively torsion module.
|
CommMonoid.primaryComponent.disjoint
theorem CommMonoid.primaryComponent.disjoint :
∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} [hp : Fact p.Prime] {p' : ℕ} [hp' : Fact p'.Prime],
p ≠ p' → Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p')
This theorem states that for any given commutative monoid `G` and any two distinct prime numbers `p` and `p'`, the `p`-primary component and the `p'`-primary component of `G` are disjoint. Here, the `p`-primary component of `G` is the submonoid consisting of elements whose order is a power of `p`. Two components are said to be disjoint if their intersection, in this context understood as the infimum in the lattice of submonoids, is the bottom element (which is the trivial submonoid containing only the identity of `G`).
More concisely: For any commutative monoid `G` and distinct prime numbers `p`, `p'`, the `p`-primary and `p'`-primary components of `G` are disjoint submonoids.
|
AddMonoid.IsTorsion.module_of_finite
theorem AddMonoid.IsTorsion.module_of_finite :
∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Ring R] [inst_2 : Finite R]
[inst_3 : Module R M], AddMonoid.IsTorsion M
The theorem `AddMonoid.IsTorsion.module_of_finite` states that for any ring `R` and any module `M` over `R`, where `M` is an additive commutative monoid and `R` is a ring with the property of being finite, the module `M` is additively torsion. In other words, every element of `M` has a finite additive order. This means for every element `m` of `M`, there exists a non-zero finite integer `n` such that `n*m = 0` in the module `M`.
More concisely: For any commutative ring with finite multiplicative order `R` and any additive commutative monoid `M` over `R`, every element of `M` has finite additive order.
|
IsTorsionFree.prod
theorem IsTorsionFree.prod :
∀ {η : Type u_3} {Gs : η → Type u_4} [inst : (i : η) → Group (Gs i)],
(∀ (i : η), Monoid.IsTorsionFree (Gs i)) → Monoid.IsTorsionFree ((i : η) → Gs i)
This theorem states that the direct product of torsion-free groups is also torsion-free. More specifically, given a family of types `Gs` indexed by `η`, each equipped with a group structure, if each group `Gs i` is torsion-free, i.e., every element of each `Gs i` that is not the identity has infinite order, then the direct product group, consisting of functions from `η` to the union of the `Gs i`, is also torsion-free.
More concisely: The direct product of a family of torsion-free groups is a torsion-free group.
|
AddIsTorsion.quotient_iff
theorem AddIsTorsion.quotient_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
Function.Surjective ⇑f → N = f.ker → AddMonoid.IsTorsion ↥N → (AddMonoid.IsTorsion H ↔ AddMonoid.IsTorsion G)
The theorem `AddIsTorsion.quotient_iff` states that for any additive groups `G` and `H`, a surjective homomorphism `f` from `G` to `H`, and a subgroup `N` of `G` that is the kernel of `f`, if all elements of `N` have finite additive order (i.e., `N` is additively torsion), then `H` is additively torsion if and only if `G` is additively torsion.
In simpler terms, it means that if every element of the subgroup `N` adds to zero after finitely many times, then each element of the entire group `G` and the quotient group `H` are both either all have a finite additive order or not. This theorem connects the property of having finite additive order between a group, its subgroup, and the quotient group under a given surjective homomorphism.
More concisely: If `f` is a surjective homomorphism from additive group `G` to `H`, `N` is the kernel of `f` and is an additively torsion subgroup of `G`, then `G` and `H` have the same property of being additively torsion or not.
|
IsTorsion.subgroup
theorem IsTorsion.subgroup :
∀ {G : Type u_1} [inst : Group G], Monoid.IsTorsion G → ∀ (H : Subgroup G), Monoid.IsTorsion ↥H
This theorem states that if a group `G` is a torsion group, then any subgroup `H` of `G` is also a torsion group. A torsion group is a type of group where every element has a finite order, meaning that for every element `g` in the group, there exists a non-zero natural number `n` such that the `n`-th power of `g` is equal to the identity element.
More concisely: A subgroup of a torsion group is a torsion group. In other words, if every element in group `G` has finite order, then every element in subgroup `H` of `G` also has finite order.
|
CommGroup.primaryComponent.isPGroup
theorem CommGroup.primaryComponent.isPGroup :
∀ {G : Type u_1} [inst : CommGroup G] {p : ℕ} [hp : Fact p.Prime], IsPGroup p ↥(CommGroup.primaryComponent G p)
The theorem states that the `p`-primary component of a commutative group is a `p`-group. In other words, in any commutative group `G` and for any prime number `p`, every element of the `p`-primary component of `G` (a subgroup of `G` composed of elements whose order is a power of `p`) has an order that is a power of `p`. This property holds true for all elements in the `p`-primary component, which categorizes the component as a `p`-group.
More concisely: In any commutative group, the subgroup of elements whose orders are powers of a prime number `p` is a `p`-group.
|
ExponentExists.isTorsion
theorem ExponentExists.isTorsion : ∀ {G : Type u_1} [inst : Group G], Monoid.ExponentExists G → Monoid.IsTorsion G := by
sorry
This theorem states that if a group has an exponent, then the group is torsion. In other words, for any group `G`, if there exists a positive integer `n` such that raising any element `g` of the group to the power `n` gives the identity element (`g^n = 1`), then all elements of the group `G` are of finite order. Here, an element being "of finite order" means that there exists some positive integer `m` such that when the element is raised to the `m`th power, it also yields the identity element.
More concisely: If a group has an element of finite order `n`, then every element in the group has finite order.
|
ExponentExists.is_add_torsion
theorem ExponentExists.is_add_torsion :
∀ {G : Type u_1} [inst : AddGroup G], AddMonoid.ExponentExists G → AddMonoid.IsTorsion G
This theorem states that given any additive group `G`, if there exists a positive integer `n` such that multiplying any element `g` of `G` by `n` gives the additive identity (i.e., 0), then all elements of the group `G` are of finite additive order. In other words, if `G` satisfies the condition of having an exponent, then `G` is torsion or periodic; every element `g` in this group can be added to itself a certain number of times to result in the group's additive identity.
More concisely: If an additive group `G` has an element of finite order `n`, then every element in `G` has finite order.
|
Monoid.IsTorsion.torsion_eq_top
theorem Monoid.IsTorsion.torsion_eq_top :
∀ {G : Type u_1} [inst : CommMonoid G], Monoid.IsTorsion G → CommMonoid.torsion G = ⊤
This theorem states that for any commutative monoid 'G', if 'G' satisfies the property of being a torsion monoid (i.e., every element in 'G' has finite order), then the torsion submonoid of 'G' is equal to the whole monoid 'G'. In other words, all elements of a torsion monoid are torsion elements.
More concisely: In a commutative monoid, the torsion submonoid equals the whole monoid if and only if every element is torsion.
|
Monoid.not_isTorsion_iff
theorem Monoid.not_isTorsion_iff : ∀ (G : Type u_1) [inst : Monoid G], ¬Monoid.IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g := by
sorry
The theorem states that a monoid is not a torsion monoid if and only if it has an element of infinite order. Here, a torsion monoid refers to a type of monoid where every element has a finite order. An element of a monoid is said to have finite order if there exists a positive integer `n` such that when the element is raised to the power `n`, it equals `1`. Conversely, an element has infinite order if no such `n` exists. Thus, the presence of an element with infinite order prevents the monoid from being a torsion monoid.
More concisely: A monoid is not torsion if and only if it contains an element of infinite order.
|
CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow
theorem CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow :
∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} [hp : Fact p.Prime] (g : ↥(CommMonoid.primaryComponent G p)),
∃ n, orderOf g = p ^ n
The theorem `CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow` states that for any given commutative monoid `G` and a prime number `p`, any element `g` of the `p`-primary component of `G` will have an order `p^n` for some integer `n`. Here, the order of an element `g`, denoted as `orderOf g`, is the smallest positive integer `n` such that `g` raised to the power of `n` is equal to the identity of the monoid; if no such `n` exists, the order is defined to be `0`. The `p`-primary component of `G` is defined to be the set of all elements in `G` whose order is a power of `p`.
More concisely: In a commutative monoid, every element in the prime-power component has an order that is a power of the prime.
|
IsTorsionFree.not_torsion
theorem IsTorsionFree.not_torsion :
∀ {G : Type u_1} [inst : Group G] [hN : Nontrivial G], Monoid.IsTorsionFree G → ¬Monoid.IsTorsion G
This theorem states that a nontrivial torsion-free group is not a torsion group. In more detail, for any group `G` which is nontrivial (i.e., it has at least one element that is not the identity), if `G` is torsion-free (meaning every element in the group that isn't the identity has infinite order), then `G` cannot be a torsion group (a group where every element has finite order).
More concisely: A nontrivial torsion-free group has no elements of finite order.
|
CommMonoid.torsion.isTorsion
theorem CommMonoid.torsion.isTorsion :
∀ {G : Type u_1} [inst : CommMonoid G], Monoid.IsTorsion ↥(CommMonoid.torsion G)
The theorem `CommMonoid.torsion.isTorsion` states that for any given type `G` that is a commutative monoid (denoted by `[inst : CommMonoid G]`), the torsion submonoid of `G` (obtained using `CommMonoid.torsion G`) is a torsion monoid. In other words, every element of the torsion submonoid of a commutative monoid has finite order. This means that for every element in the submonoid, there exists a positive integer `n` such that the element raised to the power `n` equals the identity element.
More concisely: The torsion submonoid of a commutative monoid is a submonoid of elements with finite order.
|
IsTorsion.extension_closed
theorem IsTorsion.extension_closed :
∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
N = f.ker → Monoid.IsTorsion H → Monoid.IsTorsion ↥N → Monoid.IsTorsion G
This theorem states that torsion groups are closed under extensions. Specifically, for any groups `G` and `H`, a subgroup `N` of `G`, and a group homomorphism `f` from `G` to `H`, if `N` is the kernel of `f`, and both `H` and `N` are torsion groups (that is, all of their elements have finite order), then `G` must also be a torsion group. In other words, the property of being a torsion group is preserved when extending a subgroup to the whole group, given certain conditions.
More concisely: If `G` is a group, `H` is a group with `G` being a subgroup, `N` is the kernel of a group homomorphism `f` from `G` to `H`, and both `G` and `N` are torsion groups, then `G` is also a torsion group.
|
isTorsion_of_finite
theorem isTorsion_of_finite : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Finite G], Monoid.IsTorsion G
This theorem states that all finite groups are torsion groups. In more detail, given any type `G` that has a group structure (as indicated by `[inst : Group G]`) and is finite (as indicated by `[inst_1 : Finite G]`), then `G` is also a torsion group. A torsion group is defined as a group in which every element has finite order, meaning that for every element `g` in the group, there exists a positive integer `n` such that the `n`-th power of `g` equals the group's identity element.
More concisely: A finite group is a torsion group, meaning every element has finite order.
|
AddMonoid.not_isTorsion_iff
theorem AddMonoid.not_isTorsion_iff :
∀ (G : Type u_1) [inst : AddMonoid G], ¬AddMonoid.IsTorsion G ↔ ∃ g, ¬IsOfFinAddOrder g
The theorem states that an additive monoid is not a torsion monoid if and only if there exists an element within it of infinite order. In other words, an additive monoid does not satisfy the condition that all its elements are of finite order precisely when there is at least one element in the monoid for which there does not exist a positive integer `n` such that the result of the `n`-fold addition of the element to itself (denoted `n • a`) is the additive identity (usually represented as `0` in the context of monoids).
More concisely: An additive monoid does not have the property of being torsion if and only if it contains an element of infinite order.
|
AddIsTorsion.of_surjective
theorem AddIsTorsion.of_surjective :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H},
Function.Surjective ⇑f → AddMonoid.IsTorsion G → AddMonoid.IsTorsion H
The theorem `AddIsTorsion.of_surjective` states that for any two types `G` and `H` with additive group structures, if there exists a surjective group homomorphism `f` from `G` to `H`, and all elements of `G` have finite additive order (i.e., `G` is a torsion group), then all elements of `H` also have finite additive order (i.e., `H` is also a torsion group). In simpler terms, the image of a surjective homomorphism from a torsion additive group is also a torsion additive group.
More concisely: If `G` is a torsion additive group and `f` is a surjective group homomorphism from `G` to `H`, then `H` is also a torsion additive group.
|
AddMonoid.IsTorsionFree.not_torsion
theorem AddMonoid.IsTorsionFree.not_torsion :
∀ {G : Type u_1} [inst : AddGroup G] [hN : Nontrivial G], AddMonoid.IsTorsionFree G → ¬AddMonoid.IsTorsion G := by
sorry
This theorem states that a nontrivial torsion-free additive group is not a torsion. In more detail, given any type `G` that has a group structure (`AddGroup G`) and is nontrivial (meaning that there exist at least two distinct elements), if `G` is torsion-free (meaning that the only element of `G` that has a finite additive order is the zero element), then `G` cannot be a torsion (meaning that not all elements of `G` have finite additive order).
More concisely: A nontrivial additive group with only the zero element having finite order is torsion-free and hence not a torsion group.
|
AddMonoid.not_isTorsionFree_iff
theorem AddMonoid.not_isTorsionFree_iff :
∀ {G : Type u_1} [inst : AddMonoid G], ¬AddMonoid.IsTorsionFree G ↔ ∃ g, g ≠ 0 ∧ IsOfFinAddOrder g
This theorem states that an additive monoid is not torsion-free if there exists any nontrivial element that has finite order. Here, a nontrivial element is an element that is not equal to 0, and an element is said to have finite order if there exists a positive integer n such that the n-fold sum of the element equals 0. This directly contradicts the property of being torsion-free, where only the zero element can have finite order, implying the monoid is not torsion-free.
More concisely: An additive monoid contains a nontrivial element of finite order implies the monoid is not torsion-free.
|
IsTorsionFree.subgroup
theorem IsTorsionFree.subgroup :
∀ {G : Type u_1} [inst : Group G], Monoid.IsTorsionFree G → ∀ (H : Subgroup G), Monoid.IsTorsionFree ↥H
This theorem states that if a group G is torsion-free, then any subgroup H of G is also torsion-free. Here, a group is said to be torsion-free if the only element of the group that has finite order is the identity element. In other words, no element other than the identity can be raised to some positive power to obtain the identity. Therefore, this theorem asserts that this property of being torsion-free is preserved under taking subgroups, i.e., if a group doesn't have elements of finite order, its subgroups also don't have such elements.
More concisely: If G is a torsion-free group, then every subgroup H of G is also torsion-free.
|
CommGroup.torsion_eq_torsion_submonoid
theorem CommGroup.torsion_eq_torsion_submonoid :
∀ (G : Type u_1) [inst : CommGroup G], CommMonoid.torsion G = (CommGroup.torsion G).toSubmonoid
This theorem states that, for any abelian group (G), the torsion submonoid of G is equal to the torsion subgroup of G when viewed as a submonoid. In other words, the collection of elements of G with finite order, when considered under the operations of the group (which includes inversion), forms a subgroup that coincides with the submonoid formed by considering only the monoid operations (without inversion).
More concisely: The torsion submonoid and torsion subgroup of an abelian group coincide.
|
AddCommMonoid.addTorsion.isTorsion
theorem AddCommMonoid.addTorsion.isTorsion :
∀ {G : Type u_1} [inst : AddCommMonoid G], AddMonoid.IsTorsion ↥(AddCommMonoid.addTorsion G)
This theorem states that the additive torsion submonoid of any additive commutative monoid is itself torsion. In other words, for any given type `G` that has an additive commutative monoid structure, all elements of the torsion submonoid of `G` (defined as the set of elements of `G` that have finite additive order) also have finite additive order. Here, an element is said to have finite additive order if there exists some positive integer `n` such that adding the element to itself `n` times yields the zero element.
More concisely: The additive torsion submonoid of an additive commutative monoid is torsion. In other words, all elements in the submonoid have finite additive orders.
|
Monoid.not_isTorsionFree_iff
theorem Monoid.not_isTorsionFree_iff :
∀ {G : Type u_1} [inst : Monoid G], ¬Monoid.IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
The theorem states that a nontrivial monoid is not torsion-free if and only if there exists a nontrivial element of the monoid that has finite order. In other words, for a given monoid, it is not torsion-free (meaning it has elements of finite order) if we can find an element, other than the identity, whose order is finite. Here, an element is said to have finite order if there exists a positive integer `n` such that the element raised to the power `n` equals the identity element of the monoid.
More concisely: A monoid is not torsion-free if and only if it contains a nontrivial element of finite order.
|
AddIsTorsionFree.quotient_torsion
theorem AddIsTorsionFree.quotient_torsion :
∀ (G : Type u_1) [inst : AddCommGroup G], AddMonoid.IsTorsionFree (G ⧸ AddCommGroup.torsion G)
This theorem states that for any additive commutative group `G`, when we create a quotient group by dividing `G` by its torsion subgroup, the resulting group is torsion free. Here, an additive group is called torsion free if the only element of finite order is the zero element. In other words, no other element, when added to itself a finite number of times, will yield the zero element. The "torsion subgroup" of a group is the subgroup made up of elements of finite order. Thus, the theorem is saying that if we "remove" these elements of finite order from `G` by quotienting, we will end up with a group that has no elements of finite order apart from zero.
More concisely: For any additive commutative group `G`, the quotient `G / torsionSubgroup(G)` is a torsion-free group.
|
IsTorsionFree.quotient_torsion
theorem IsTorsionFree.quotient_torsion :
∀ (G : Type u_1) [inst : CommGroup G], Monoid.IsTorsionFree (G ⧸ CommGroup.torsion G)
This theorem states that for any commutative group `G`, the quotient group formed by dividing `G` with its torsion subgroup is a torsion-free group. Here, a torsion-free group is defined as a group in which only the identity element (1) has a finite order. In other words, the result of dividing a group by its torsion subgroup removes all elements of finite order (except for the identity), thereby creating a group where every non-identity element has infinite order, i.e., a torsion-free group.
More concisely: For any commutative group `G`, the quotient `G / torsion Subgroup(G)` is a torsion-free group.
|
AddMonoid.IsTorsion.torsion_eq_top
theorem AddMonoid.IsTorsion.torsion_eq_top :
∀ {G : Type u_1} [inst : AddCommMonoid G], AddMonoid.IsTorsion G → AddCommMonoid.addTorsion G = ⊤
The theorem states that for any type `G` that has an instance of a commutative additive monoid, if `G` also satisfies the property of being a torsion monoid - where every element has a finite additive order, then the torsion submonoid of `G` is equal to the entire monoid. In other words, if every element in an additive commutative monoid has a finite order, then the submonoid comprising these elements of finite order is equal to the whole monoid.
More concisely: If `G` is a commutative additive monoid with every element having finite additive order, then the submonoid of elements of finite order equals the entire monoid `G`.
|
IsTorsion.quotient_iff
theorem IsTorsion.quotient_iff :
∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
Function.Surjective ⇑f → N = f.ker → Monoid.IsTorsion ↥N → (Monoid.IsTorsion H ↔ Monoid.IsTorsion G)
The theorem `IsTorsion.quotient_iff` states that for any two types `G` and `H` (representing groups), a subgroup `N` of `G`, and a surjective group homomorphism `f` from `G` to `H`, if `N` is the kernel of `f` and all elements of `N` have finite order (i.e., `N` is a torsion subgroup), then the group `H` is a torsion group if and only if the group `G` is a torsion group.
In mathematical terms, a group is said to be a torsion group if all its elements have finite order, that is, for each element, there exists a positive integer such that raising the element to this power gives the identity. The theorem connects the property of being a torsion group for the original group, the image group under the homomorphism, and the kernel of the homomorphism.
More concisely: If `G` is a group, `N` is a torsion subgroup of `G` that is the kernel of a surjective group homomorphism `f: G -> H`, then `G` and `H` are both torsion groups.
|
IsTorsion.addSubgroup
theorem IsTorsion.addSubgroup :
∀ {G : Type u_1} [inst : AddGroup G], AddMonoid.IsTorsion G → ∀ (H : AddSubgroup G), AddMonoid.IsTorsion ↥H := by
sorry
This theorem states that if we have an additive torsion group G, then any subgroup H of that group G is also an additive torsion group. In more detail, given a type `G` that is an additive group and is torsion (meaning every element of the group has finite additive order), for any additive subgroup `H` of `G`, the subgroup `H` is also torsion. In mathematical terms, this means that for every element in the subgroup `H`, there exists a non-zero integer `n` such that `n * h = 0` for that element `h`.
More concisely: If `G` is an additive torsion group, then any of its additive subgroups are also torsion groups.
|