Structures · Algebra
IsCyclic
A group is called cyclic if it is generated by a single element. [Wikidata Q245462](https://www.wikidata.org/wiki/Q245462)
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds exists_zpow_surjective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Units
- AlgEquiv
- FreeGroup
- Abelianization
- Subtype
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by75
- isCyclic_of_surjective
- IsCyclic.exists_generator
- LinearOrderedCommGroup.Subgroup.genLTOne
- IsCyclic.exponent_eq_card
- IsCyclic.mulAutMulEquiv
- LinearOrderedCommGroup.Subgroup.genLTOne_unique
- Subgroup.isCyclic_of_le
- IsCyclic.exists_zpow_surjective
- exists_zpow_surjective
- IsCyclic.exists_ofOrder_eq_natCard
- MonoidHom.map_cyclic
- LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top
- IsCyclic.card_pow_eq_one_le
- IsCyclic.index_powMonoidHom_range
- IsCyclic.commGroup
- LinearOrderedCommGroup.Subgroup.exists_generator_lt_one
- isCyclic_left_of_prod
- MulDistribMulAction.toMonoidHomZModOfIsCyclic
- LinearOrderedCommGroup.Subgroup.genLTOne_lt_one
- LinearOrderedCommGroup.genLTOne
- isCyclic_of_injective
- Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial
- isCyclic_right_of_prod
- LinearOrderedCommGroup.Subgroup.genLTOne.congr_simp
- MulChar.equiv_rootsOfUnity
- IsCyclic.monoidHom_mulEquiv_rootsOfUnity
- Group.isCyclic_of_coprime_card_ker
- MonoidHom.isMulCommutative_of_isCyclic_of_ker_le_center
- Group.isCyclic_of_coprime_card_range_card_ker
- coprime_card_of_isCyclic_prod
- LinearOrderedCommGroup.Subgroup.genLTOne_mem
- Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator
- Valuation.valuationSubring_not_isField
- Sylow.normalizer_le_centralizer_or_le_commutator
- mulEquivOfCyclicCardEq
- groupCohomology.exists_div_of_norm_eq_one
- Sylow.le_center_or_le_commutator
- exists_root_adjoin_eq_top_of_isCyclic
- IsCyclic.card_powMonoidHom_range
- exists_pow_ne_one_of_isCyclic
- MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply
- IsCyclic.exists_apply_ne_one
- IsCyclic.index_powMonoidHom_ker
- isMulCommutative_of_isCyclic_quotient_center_self
- Sylow.commutator_eq_bot_or_commutator_eq_self
- IsCyclic.card_powMonoidHom_ker
- IsCyclic.monoidHom_equiv_self
- IsCyclic.exists_monoid_generator
- IsPGroup.commutator_eq_bot_or_commutator_eq_self
- IsCyclic.card_mulAut
Ancestors0
No ancestors.