Nontrivial.of_not_isAddCyclic
theorem Nontrivial.of_not_isAddCyclic : ∀ {α : Type u} [inst : AddGroup α], ¬IsAddCyclic α → Nontrivial α
This theorem states that for any type 'α' that forms an additive group, if this group is not cyclic, then it is non-trivial. In other words, if an additive group does not revolve back to its initial element after a certain number of additions (i.e., it's not cyclic), then it must contain at least two distinct elements and therefore is non-trivial.
More concisely: If an additive group of type 'α' is not cyclic, then it has at least two distinct elements.
|
orderOf_eq_card_of_forall_mem_zpowers
theorem orderOf_eq_card_of_forall_mem_zpowers :
∀ {α : Type u} [inst : Group α] [inst_1 : Fintype α] {g : α},
(∀ (x : α), x ∈ Subgroup.zpowers g) → orderOf g = Fintype.card α
The theorem `orderOf_eq_card_of_forall_mem_zpowers` states that for any type `α` that forms a group (`Group α`) and is finitely enumerable (`Fintype α`), and for any element `g` of this group, if every element `x` of the group is in the subgroup generated by `g` (i.e., every element can be expressed as some power of `g`), then the order of the element `g` (the smallest positive integer `n` such that `g` to the power `n` equals the identity element, or `0` if no such `n` exists) is equal to the number of elements in the group `α`. In other words, when a group element generates all elements in the group, its order equals the size of the group.
More concisely: If `α` is a finitely enumerable group, then the order of any element `g` generating all elements of `α` is equal to the cardinality of `α`.
|
commutative_of_add_cyclic_center_quotient
theorem commutative_of_add_cyclic_center_quotient :
∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : IsAddCyclic H] (f : G →+ H),
f.ker ≤ AddSubgroup.center G → ∀ (a b : G), a + b = b + a
The theorem `commutative_of_add_cyclic_center_quotient` states that for any additive groups `G` and `H`, where `H` is cyclic, and for any additive group homomorphism `f` from `G` to `H`, if the kernel of `f` is a subset of the center of `G`, then `G` is a commutative group. In other words, for any two elements `a` and `b` from `G`, the operation `a + b` is equal to `b + a`. This theorem is an alias of the theorem `commutative_of_addCyclic_center_quotient`, and it's suggested to also see `addCommGroup_of_cycle_center_quotient` for the additive commutative group instance.
More concisely: If an additive group `G` with cyclic subgroup `H` and homomorphism `f` from `G` to `H` has kernel contained in `G`'s center, then `G` is commutative.
|
isAddCyclic_of_prime_card
theorem isAddCyclic_of_prime_card :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : Fintype α] {p : ℕ} [hp : Fact p.Prime],
Fintype.card α = p → IsAddCyclic α
The theorem `isAddCyclic_of_prime_card` states that for any finite additive group `α` of prime order `p`, the group `α` is cyclic. In other words, if the number of elements in the group `α` (expressed as `Fintype.card α`) is equal to a prime number `p`, then the group `α` follows a cyclical structure, that is, there exists an element in `α` such that every other element in the group can be obtained by repeatedly adding this particular element to itself.
More concisely: A finite additive group of prime order is cyclic.
|
not_isCyclic_iff_exponent_eq_prime
theorem not_isCyclic_iff_exponent_eq_prime :
∀ {α : Type u} [inst : Group α] {p : ℕ}, p.Prime → Nat.card α = p ^ 2 → (¬IsCyclic α ↔ Monoid.exponent α = p) := by
sorry
The theorem states that for any type `α` that forms a group, and for any natural number `p` that is prime, if the cardinality of `α` equals `p` squared, then `α` is not a cyclic group if and only if the exponent of `α` equals `p`. In mathematical terms, a group of order `p^2`, where `p` is a prime number, is not a cyclic group if and only if its exponent is `p`. Here, the exponent of a group is defined as the smallest positive integer `n` such that raising any element of the group to the power `n` gives the identity element of the group; if no such `n` exists, the exponent is zero by convention.
More concisely: A group of prime order p^2 is not cyclic if and only if its exponent equals p.
|
isCyclic_of_orderOf_eq_card
theorem isCyclic_of_orderOf_eq_card :
∀ {α : Type u} [inst : Group α] [inst_1 : Fintype α] (x : α), orderOf x = Fintype.card α → IsCyclic α
The theorem `isCyclic_of_orderOf_eq_card` states that for any given type `α` that has a group structure (`Group α`) and is a finite type (`Fintype α`), if there exists an element `x` in `α` whose order (`orderOf x`) is equal to the number of elements in `α` (`Fintype.card α`), then `α` is a cyclic group (`IsCyclic α`). In simpler terms, it says that if the order of an element in a finite group equals the size of the group, then the group is cyclic.
More concisely: If a finite group of order `n` has an element of order `n`, then the group is cyclic.
|
addOrderOf_eq_card_of_forall_mem_zmultiples
theorem addOrderOf_eq_card_of_forall_mem_zmultiples :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : Fintype α] {g : α},
(∀ (x : α), x ∈ AddSubgroup.zmultiples g) → addOrderOf g = Fintype.card α
The theorem `addOrderOf_eq_card_of_forall_mem_zmultiples` states that for any type `α` that has an additive group structure and is finite (`Fintype`), given an element `g` of `α`, if every element `x` of `α` is in the subgroup generated by `g` (i.e., `x` is an integer multiple of `g`), then the order of `g`, denoted by `addOrderOf g` (the smallest positive integer `n` such that `n` times `g` equals the additive identity, or `0` if no such `n` exists), is equal to the total number of elements in `α`, given by `Fintype.card α`.
More concisely: For any finite additive group `α` and any element `g` in `α` such that every element in `α` is a multiple of `g`, the order of `g` equals the cardinality of `α`.
|
IsAddCyclic.exponent_eq_card
theorem IsAddCyclic.exponent_eq_card :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : IsAddCyclic α] [inst_2 : Fintype α],
AddMonoid.exponent α = Fintype.card α
The theorem `IsAddCyclic.exponent_eq_card` states that for any type `α` that forms an Additive Group and is Additive Cyclic (i.e., there is an element in `α`, whose repeated addition generates all elements in `α`) and also is a Finite Type (i.e., `α` has a finite number of distinct elements), the exponent of the Additive Monoid of `α` is equal to the number of elements in `α`. In other words, the smallest positive integer `n` such that adding any element from the group to itself `n` times results in the additive identity element (zero), is equal to the total number of elements in the group, if `α` has these properties.
More concisely: For any finite, additive group `α` that is additively cyclic, the order of its additive monoid equals its number of elements.
|
commutative_of_cyclic_center_quotient
theorem commutative_of_cyclic_center_quotient :
∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [inst_2 : IsCyclic H] (f : G →* H),
f.ker ≤ Subgroup.center G → ∀ (a b : G), a * b = b * a
The theorem "commutative_of_cyclic_center_quotient" states that for any two groups G and H, where H is cyclic, and a given group homomorphism f from G to H, if the kernel of f is a subset of the center of G, then G is a commutative group. In other words, the multiplication of any two elements in G is commutative, i.e., for any two elements a and b in G, the product of a and b is equal to the product of b and a.
The center of a group G is the set of elements that commute with all elements in G. The kernel of a group homomorphism is the set of elements in the domain that map to the identity in the codomain. A group is cyclic if it is generated by a single element.
More concisely: If group homomorphism f from commutative group G to cyclic group H has kernel contained in the center of G, then G is commutative.
|
isSimpleGroup_of_prime_card
theorem isSimpleGroup_of_prime_card :
∀ {α : Type u} [inst : Group α] [inst_1 : Fintype α] {p : ℕ} [hp : Fact p.Prime],
Fintype.card α = p → IsSimpleGroup α
The theorem states that if we have a finite group, represented by the type variable `α`, and the order (size) of this group is equal to a prime number `p`, then this group is a simple group. A simple group is a nontrivial group whose only normal subgroups are the trivial group and the group itself. In this context, a prime number is a natural number greater than 1 that has no positive divisors other than 1 and itself. The order of a group is the number of its elements, and a finite group is a group with a finite number of elements. The theorem basically establishes the relationship between prime order and the simplicity of a group.
More concisely: A finite group of prime order is a simple group.
|
Nontrivial.of_not_isCyclic
theorem Nontrivial.of_not_isCyclic : ∀ {α : Type u} [inst : Group α], ¬IsCyclic α → Nontrivial α
This theorem states that in any multiplicative group of a certain type `α`, if the group is not cyclic, then it must be nontrivial. Here, `Nontrivial α` means the group contains at least two distinct elements, and `IsCyclic α` means the group is generated by a single element. In other words, a non-cyclic group cannot be a trivial group (a group with only one element).
More concisely: In a multiplicative group of type `α`, if `IsCyclic α` is false, then `Nontrivial α` holds.
|
isSimpleAddGroup_of_prime_card
theorem isSimpleAddGroup_of_prime_card :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : Fintype α] {p : ℕ} [hp : Fact p.Prime],
Fintype.card α = p → IsSimpleAddGroup α
This theorem states that for any given type 'α' which holds an additive group structure and is also finite, if the number of elements (or the 'order') in this group is equal to a prime number 'p', then this additive group is simple. Simple in this context means the group has no non-trivial normal subgroups; a group is said to be trivial if it contains only the identity element. The prime number 'p' is given as a fact, which is a way in Lean to assume a proposition to be true.
More concisely: For any finite additive group of prime order 'p', there are no non-trivial normal subgroups.
|
isCyclic_of_prime_card
theorem isCyclic_of_prime_card :
∀ {α : Type u} [inst : Group α] [inst_1 : Fintype α] {p : ℕ} [hp : Fact p.Prime], Fintype.card α = p → IsCyclic α
The theorem `isCyclic_of_prime_card` states that for any finite group characterized by the type `α` and for any natural number `p` that is known to be prime, if the number of elements in the group (given by `Fintype.card α`) is equal to `p`, then the group is cyclic. In other words, a group of prime order is always cyclic.
More concisely: A finite group of prime order is cyclic.
|