Cyclic groups #
A group G
is called cyclic if there exists an element g : G
such that every element of G
is of
the form g ^ n
for some n : ℕ
. This file only deals with the predicate on a group to be cyclic.
For the concrete cyclic group of order n
, see data.zmod.basic
.
Main definitions #
is_cyclic
is a predicate on a group stating that the group is cyclic.
Main statements #
is_cyclic_of_prime_card
proves that a finite group of prime order is cyclic.is_simple_group_of_prime_card
,is_simple_group.is_cyclic
, andis_simple_group.prime_card
classify finite simple abelian groups.is_cyclic.exponent_eq_card
: For a finite cyclic groupG
, the exponent is equal to the group's cardinality.is_cyclic.exponent_eq_zero_of_infinite
: Infinite cyclic groups have exponent zero.is_cyclic.iff_exponent_eq_card
: A finite commutative group is cyclic iff its exponent is equal to its cardinality.
Tags #
cyclic group
- exists_generator : ∃ (g : α), ∀ (x : α), x ∈ add_subgroup.zmultiples g
A group is called cyclic if it is generated by a single element.
Instances of this typeclass
- exists_generator : ∃ (g : α), ∀ (x : α), x ∈ subgroup.zpowers g
A group is called cyclic if it is generated by a single element.
A cyclic group is always commutative. This is not an instance
because often we have
a better proof of add_comm_group
.
Equations
- is_add_cyclic.add_comm_group = {add := add_group.add hg, add_assoc := _, zero := add_group.zero hg, zero_add := _, add_zero := _, nsmul := add_group.nsmul hg, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg hg, sub := add_group.sub hg, sub_eq_add_neg := _, zsmul := add_group.zsmul hg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
A cyclic group is always commutative. This is not an instance
because often we have a better
proof of comm_group
.
Equations
- is_cyclic.comm_group = {mul := group.mul hg, mul_assoc := _, one := group.one hg, one_mul := _, mul_one := _, npow := group.npow hg, npow_zero' := _, npow_succ' := _, inv := group.inv hg, div := group.div hg, div_eq_mul_inv := _, zpow := group.zpow hg, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
A finite group of prime order is cyclic.
A finite group of prime order is cyclic.
A finite group of prime order is simple.
A finite group of prime order is simple.
A group is commutative if the quotient by
the center is cyclic. Also see add_comm_group_of_cycle_center_quotient
for the add_comm_group
instance.
A group is commutative if the quotient by the center is cyclic.
Also see comm_group_of_cycle_center_quotient
for the comm_group
instance.
A group is commutative if the quotient by the center is cyclic.
Equations
- comm_group_of_cycle_center_quotient f hf = {mul := group.mul (show group G, from _inst_1), mul_assoc := _, one := group.one (show group G, from _inst_1), one_mul := _, mul_one := _, npow := group.npow (show group G, from _inst_1), npow_zero' := _, npow_succ' := _, inv := group.inv (show group G, from _inst_1), div := group.div (show group G, from _inst_1), div_eq_mul_inv := _, zpow := group.zpow (show group G, from _inst_1), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
A group is commutative if the quotient by the center is cyclic.
Equations
- commutative_of_add_cycle_center_quotient f hf = {add := add_group.add (show add_group G, from _inst_1), add_assoc := _, zero := add_group.zero (show add_group G, from _inst_1), zero_add := _, add_zero := _, nsmul := add_group.nsmul (show add_group G, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (show add_group G, from _inst_1), sub := add_group.sub (show add_group G, from _inst_1), sub_eq_add_neg := _, zsmul := add_group.zsmul (show add_group G, from _inst_1), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}