Mathlib Map

Theorems · Theorem · group theory

isCyclic_of_orderOf_eq_card

∀ {α : Type u_1} [inst : Group α] [Finite α] (x : α), orderOf x = Nat.card α → IsCyclic α
Defined in
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Cited by
4 results in Mathlib
Foundations
Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupFinite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsCyclic.of_exponent_eq_card · cited by 1IsCyclic.of_exponent_eq_c…isCyclic_of_card_pow_eq_one_le · cited by 1isCyclic_of_card_pow_eq_o…not_isCyclic_iff_exponent_eq_prime · cited by 0not_isCyclic_iff_exponent…QuaternionGroup.quaternionGroup_one_isCyclic · cited by 0QuaternionGroup.quaternio…Group · cited by 6238GroupFinite · cited by 3029FiniteNat.card · cited by 844Nat.cardorderOf · cited by 324orderOfIsCyclic · cited by 122IsCyclicisCyclic_iff_exists_orderOf_eq_natCard · cited by 3isCyclic_iff_exists_order…isCyclic_of_orderOf_eq_cardCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.